src/HOL/Transcendental.thy
changeset 56217 dc429a5b13c4
parent 56213 e5720d3c18f0
child 56261 918432e3fcfa
     1.1 --- a/src/HOL/Transcendental.thy	Wed Mar 19 14:55:47 2014 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 19 17:06:02 2014 +0000
     1.3 @@ -2396,15 +2396,6 @@
     1.4    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
     1.5  qed
     1.6  
     1.7 -lemma real_mult_inverse_cancel:
     1.8 -     "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
     1.9 -      ==> inverse x * y < inverse x1 * u"
    1.10 -  by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)
    1.11 -
    1.12 -lemma real_mult_inverse_cancel2:
    1.13 -     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
    1.14 -  by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
    1.15 -
    1.16  lemmas realpow_num_eq_if = power_eq_if
    1.17  
    1.18  lemma sumr_pos_lt_pair:
    1.19 @@ -3208,7 +3199,7 @@
    1.20  
    1.21  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
    1.22    apply (rule power_inverse [THEN subst])
    1.23 -  apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
    1.24 +  apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
    1.25    apply (auto dest: field_power_not_zero
    1.26            simp add: power_mult_distrib distrib_right power_divide tan_def
    1.27                      mult_assoc power_inverse [symmetric])