equal
deleted
inserted
replaced
49 by (induct_tac "k" 1); |
49 by (induct_tac "k" 1); |
50 by (Auto_tac); |
50 by (Auto_tac); |
51 qed "fact_less_mono"; |
51 qed "fact_less_mono"; |
52 |
52 |
53 Goal "0 < inverse (real (fact n))"; |
53 Goal "0 < inverse (real (fact n))"; |
54 by (auto_tac (claset(),simpset() addsimps [real_inverse_gt_0])); |
54 by (auto_tac (claset(),simpset() addsimps [positive_imp_inverse_positive])); |
55 qed "inv_real_of_nat_fact_gt_zero"; |
55 qed "inv_real_of_nat_fact_gt_zero"; |
56 Addsimps [inv_real_of_nat_fact_gt_zero]; |
56 Addsimps [inv_real_of_nat_fact_gt_zero]; |
57 |
57 |
58 Goal "0 <= inverse (real (fact n))"; |
58 Goal "0 <= inverse (real (fact n))"; |
59 by (auto_tac (claset() addIs [order_less_imp_le],simpset())); |
59 by (auto_tac (claset() addIs [order_less_imp_le],simpset())); |