equal
deleted
inserted
replaced
113 done |
113 done |
114 |
114 |
115 lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" |
115 lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" |
116 apply (simp (no_asm) add: right_distrib) |
116 apply (simp (no_asm) add: right_distrib) |
117 apply (rule add_less_cancel_left [of "-r", THEN iffD1]) |
117 apply (rule add_less_cancel_left [of "-r", THEN iffD1]) |
118 apply (auto intro: mult_pos |
118 apply (auto intro: mult_pos_pos |
119 simp add: add_assoc [symmetric] neg_less_0_iff_less) |
119 simp add: add_assoc [symmetric] neg_less_0_iff_less) |
120 done |
120 done |
121 |
121 |
122 lemma real_mult_add_one_minus_ge_zero: |
122 lemma real_mult_add_one_minus_ge_zero: |
123 "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" |
123 "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" |