equal
deleted
inserted
replaced
204 apply (rule mult_pos_pos) |
204 apply (rule mult_pos_pos) |
205 apply (rule add_pos_nonneg) |
205 apply (rule add_pos_nonneg) |
206 apply auto |
206 apply auto |
207 done |
207 done |
208 also have "... = exp (-x)" |
208 also have "... = exp (-x)" |
209 by (auto simp add: exp_minus real_divide_def) |
209 by (auto simp add: exp_minus divide_inverse) |
210 finally have "1 - x <= exp (- x)" . |
210 finally have "1 - x <= exp (- x)" . |
211 also have "1 - x = exp (ln (1 - x))" |
211 also have "1 - x = exp (ln (1 - x))" |
212 proof - |
212 proof - |
213 have "0 < 1 - x" |
213 have "0 < 1 - x" |
214 by (insert b, auto) |
214 by (insert b, auto) |