equal
deleted
inserted
replaced
18 |
18 |
19 lemma fact_gt_zero [simp]: "0 < fact n" |
19 lemma fact_gt_zero [simp]: "0 < fact n" |
20 by (induct n) auto |
20 by (induct n) auto |
21 |
21 |
22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0" |
22 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0" |
23 by simp |
23 by (simp add: neq0_conv) |
24 |
24 |
25 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" |
25 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0" |
26 by auto |
26 by auto |
27 |
27 |
28 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" |
28 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" |