equal
deleted
inserted
replaced
87 also have "\<dots> / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))" |
87 also have "\<dots> / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))" |
88 using n_pos \<open>t \<ge> 0\<close> by (subst divide_ennreal) auto |
88 using n_pos \<open>t \<ge> 0\<close> by (subst divide_ennreal) auto |
89 also have "t ^ n / n / fact (card A) = t ^ n / fact n" |
89 also have "t ^ n / n / fact (card A) = t ^ n / fact n" |
90 by (simp add: n_def) |
90 by (simp add: n_def) |
91 also have "n = card (insert b A)" |
91 also have "n = card (insert b A)" |
92 using insert.hyps by (subst card_insert) (auto simp: n_def) |
92 using insert.hyps by (subst card.insert_remove) (auto simp: n_def) |
93 finally show ?case . |
93 finally show ?case . |
94 qed |
94 qed |
95 |
95 |
96 end |
96 end |
97 |
97 |