src/HOL/Real/RealPow.thy
changeset 14288 d149e3cbdb39
parent 14269 502a7c95de73
child 14304 cc0b4bbfbc43
     1.1 --- a/src/HOL/Real/RealPow.thy	Wed Dec 10 14:29:44 2003 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Wed Dec 10 15:59:34 2003 +0100
     1.3 @@ -146,9 +146,10 @@
     1.4  
     1.5  lemma realpow_Suc_less [rule_format]:
     1.6       "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
     1.7 -  by (induct_tac "n", auto)
     1.8 +  by (induct_tac "n", auto simp add: mult_less_cancel_left)
     1.9  
    1.10 -lemma realpow_Suc_le [rule_format]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
    1.11 +lemma realpow_Suc_le [rule_format]:
    1.12 +     "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
    1.13  apply (induct_tac "n")
    1.14  apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
    1.15  done
    1.16 @@ -188,7 +189,7 @@
    1.17  by (induct_tac "n", auto)
    1.18  
    1.19  lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
    1.20 -by (induct_tac "n", auto)
    1.21 +by (induct_tac "n", auto simp add: mult_less_cancel_left)
    1.22  
    1.23  lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
    1.24  by (blast intro!: order_less_imp_le realpow_less_Suc)