equal
deleted
inserted
replaced
40 apply blast |
40 apply blast |
41 done |
41 done |
42 |
42 |
43 lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n" |
43 lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n" |
44 apply (unfold cd_def) |
44 apply (unfold cd_def) |
45 apply (blast intro: dvd_diff dest: dvd_diffD) |
45 apply (fastsimp dest: dvd_diffD) |
46 done |
46 done |
47 |
47 |
48 lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)" |
48 lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)" |
49 apply (unfold cd_def) |
49 apply (unfold cd_def) |
50 apply (blast intro: dvd_diff dest: dvd_diffD) |
50 apply (fastsimp dest: dvd_diffD) |
51 done |
51 done |
52 |
52 |
53 |
53 |
54 subsubsection {* gcd *} |
54 subsubsection {* gcd *} |
55 |
55 |