src/HOL/GCD.thy
changeset 34223 dce32a1e05fe
parent 34222 e33ee7369ecb
child 34915 7894c7dab132
     1.1 --- a/src/HOL/GCD.thy	Fri Jan 01 17:21:44 2010 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Jan 01 19:15:43 2010 +0100
     1.3 @@ -1689,11 +1689,10 @@
     1.4    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
     1.5     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
     1.6  apply(auto simp add:inj_on_def)
     1.7 -apply (metis coprime_dvd_mult_nat dvd.eq_iff gcd_lcm_lattice_nat.inf_sup_absorb
     1.8 -     gcd_semilattice_nat.inf_le2 lcm_proj2_iff_nat nat_mult_1 prod_gcd_lcm_nat)
     1.9 -apply (metis coprime_dvd_mult_nat gcd_proj1_if_dvd_nat
    1.10 -       gcd_semilattice_nat.inf_commute lcm_dvd1_nat nat_mult_1
    1.11 -       nat_mult_commute prod_gcd_lcm_nat)
    1.12 +apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    1.13 +             dvd.neq_le_trans dvd_triv_left)
    1.14 +apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    1.15 +             dvd.neq_le_trans dvd_triv_right mult_commute)
    1.16  done
    1.17  
    1.18  text{* Nitpick: *}