src/HOL/Transcendental.thy
changeset 46240 933f35c4e126
parent 45915 0e5a87b772f9
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Transcendental.thy	Tue Jan 17 11:15:36 2012 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Jan 17 16:30:54 2012 +0100
     1.3 @@ -1478,9 +1478,6 @@
     1.4    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
     1.5  qed
     1.6  
     1.7 -lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
     1.8 -by simp
     1.9 -
    1.10  lemma real_mult_inverse_cancel:
    1.11       "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
    1.12        ==> inverse x * y < inverse x1 * u"
    1.13 @@ -1516,11 +1513,7 @@
    1.14  unfolding One_nat_def
    1.15  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
    1.16              del: fact_Suc)
    1.17 -apply (rule real_mult_inverse_cancel2)
    1.18 -apply (simp del: fact_Suc)
    1.19 -apply (simp del: fact_Suc)
    1.20 -apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
    1.21 -apply (subst fact_lemma)
    1.22 +apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
    1.23  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
    1.24  apply (simp only: real_of_nat_mult)
    1.25  apply (rule mult_strict_mono, force)