equal
deleted
inserted
replaced
63 done |
63 done |
64 also have "... <= (1/2) * inverse(fact (n + 2))" |
64 also have "... <= (1/2) * inverse(fact (n + 2))" |
65 apply (rule mult_right_mono) |
65 apply (rule mult_right_mono) |
66 apply (subst inverse_eq_divide) |
66 apply (subst inverse_eq_divide) |
67 apply simp |
67 apply simp |
68 apply (rule inv_real_of_nat_fact_ge_zero) |
68 apply (simp del: fact_Suc) |
69 done |
69 done |
70 finally show ?thesis . |
70 finally show ?thesis . |
71 qed |
71 qed |
72 moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" |
72 moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" |
73 by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b) |
73 by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b) |