src/HOL/Decision_Procs/Rat_Pair.thy
 changeset 67051 e7e54a0b9197 parent 62390 842917225d56 child 67123 3fe40ff1b921
```     1.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -51,7 +51,8 @@
1.4      from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
1.5      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
1.6      from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
1.7 -    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
1.8 +    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
1.9 +      by simp
1.10      from ab consider "b < 0" | "b > 0" by arith
1.11      then show ?thesis
1.12      proof cases
1.13 @@ -198,6 +199,8 @@
1.14      from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
1.15      have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
1.17 +    then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
1.18 +      by (simp_all add: coprime_iff_gcd_eq_1)
1.19      from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
1.20        apply -
1.21        apply algebra
1.22 @@ -205,11 +208,11 @@
1.23        apply simp
1.24        apply algebra
1.25        done
1.26 -    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
1.27 -        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
1.28 -      have eq1: "b = b'" using pos by arith
1.29 -      with eq have "a = a'" using pos by simp
1.30 -      with eq1 show ?thesis by (simp add: x y)
1.31 +    then have eq1: "b = b'"
1.32 +      using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
1.33 +      by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
1.34 +    with eq have "a = a'" using pos by simp
1.35 +    with \<open>b = b'\<close> show ?thesis by (simp add: x y)
1.36    qed
1.37    show ?lhs if ?rhs
1.38      using that by simp
```