equal
deleted
inserted
replaced
69 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; |
69 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; |
70 |
70 |
71 |
71 |
72 (*Maximality: for all m,n,k naturals, |
72 (*Maximality: for all m,n,k naturals, |
73 if k divides m and k divides n then k divides gcd(m,n)*) |
73 if k divides m and k divides n then k divides gcd(m,n)*) |
74 lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)" |
74 lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)" |
75 apply (induct_tac m n rule: gcd_induct) |
75 apply (induct_tac m n rule: gcd_induct) |
76 apply (simp_all add: gcd_non_0 dvd_mod); |
76 apply (simp_all add: gcd_non_0 dvd_mod); |
77 done; |
77 done; |
78 |
78 |
79 lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)" |
79 lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)" |