--- a/src/HOL/Library/Primes.thy Wed Jun 13 16:28:40 2001 +0200
+++ b/src/HOL/Library/Primes.thy Wed Jun 13 16:29:51 2001 +0200
@@ -72,17 +72,6 @@
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
-lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
-proof
- have "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" by simp
- also assume "gcd (m, n) = 0"
- finally have "0 dvd m \<and> 0 dvd n" .
- thus "m = 0 \<and> n = 0" by (simp add: dvd_0_left)
-next
- assume "m = 0 \<and> n = 0"
- thus "gcd (m, n) = 0" by simp
-qed
-
text {*
\medskip Maximality: for all @{term m}, @{term n}, @{term k}
@@ -99,6 +88,9 @@
apply (blast intro!: gcd_greatest intro: dvd_trans)
done
+lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
+ by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
+
text {*
\medskip Function gcd yields the Greatest Common Divisor.