src/HOL/Transcendental.thy
changeset 38642 8fa437809c67
parent 37887 2ae085b07f2f
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Transcendental.thy	Sun Aug 22 14:27:30 2010 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Aug 23 11:17:13 2010 +0200
     1.3 @@ -2790,7 +2790,7 @@
     1.4  
     1.5  lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
     1.6  proof -
     1.7 -  from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
     1.8 +  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
     1.9    have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
    1.10    thus ?thesis using zero_le_power2 by auto
    1.11  qed