equal
deleted
inserted
replaced
56 lemma gcd_nnn: "0<n ==> n = gcd n n" |
56 lemma gcd_nnn: "0<n ==> n = gcd n n" |
57 apply (unfold gcd_def) |
57 apply (unfold gcd_def) |
58 apply (frule cd_nnn) |
58 apply (frule cd_nnn) |
59 apply (rule some_equality [symmetric]) |
59 apply (rule some_equality [symmetric]) |
60 apply (blast dest: cd_le) |
60 apply (blast dest: cd_le) |
61 apply (blast intro: le_anti_sym dest: cd_le) |
61 apply (blast intro: le_antisym dest: cd_le) |
62 done |
62 done |
63 |
63 |
64 lemma gcd_swap: "gcd m n = gcd n m" |
64 lemma gcd_swap: "gcd m n = gcd n m" |
65 apply (simp add: gcd_def cd_swap) |
65 apply (simp add: gcd_def cd_swap) |
66 done |
66 done |