src/HOL/GCD.thy
changeset 33946 fcc20072df9a
parent 33657 a4179bf442d1
child 34030 829eb528b226
     1.1 --- a/src/HOL/GCD.thy	Fri Dec 04 08:26:25 2009 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Dec 04 08:52:09 2009 +0100
     1.3 @@ -779,14 +779,6 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 -lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
     1.8 -  using coprime_dvd_mult_iff_nat[of d a b]
     1.9 -  by (auto simp add: mult_commute)
    1.10 -
    1.11 -lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
    1.12 -  using coprime_dvd_mult_iff_int[of d a b]
    1.13 -  by (auto simp add: mult_commute)
    1.14 -
    1.15  lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
    1.16    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
    1.17  proof-