--- a/src/HOL/GCD.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/GCD.thy Sat Dec 17 15:22:13 2016 +0100
@@ -639,7 +639,6 @@
using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
qed
-
lemma divides_mult:
assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
shows "a * b dvd c"
@@ -695,6 +694,10 @@
using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
by blast
+lemma coprime_mul_eq':
+ "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
+ using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
+
lemma gcd_coprime:
assumes c: "gcd a b \<noteq> 0"
and a: "a = a' * gcd a b"
@@ -958,6 +961,24 @@
ultimately show ?thesis by (rule that)
qed
+lemma coprime_crossproduct':
+ fixes a b c d
+ assumes "b \<noteq> 0"
+ assumes unit_factors: "unit_factor b = unit_factor d"
+ assumes coprime: "coprime a b" "coprime c d"
+ shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+ assume eq: "a * d = b * c"
+ hence "normalize a * normalize d = normalize c * normalize b"
+ by (simp only: normalize_mult [symmetric] mult_ac)
+ with coprime have "normalize b = normalize d"
+ by (subst (asm) coprime_crossproduct) simp_all
+ from this and unit_factors show "b = d"
+ by (rule normalize_unit_factor_eqI)
+ from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+ with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
end
class ring_gcd = comm_ring_1 + semiring_gcd