equal
deleted
inserted
replaced
112 le_Suc_eq, binomial_eq_0])); |
112 le_Suc_eq, binomial_eq_0])); |
113 qed_spec_mp "Suc_times_binomial_eq"; |
113 qed_spec_mp "Suc_times_binomial_eq"; |
114 |
114 |
115 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
115 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"; |
116 by (asm_simp_tac |
116 by (asm_simp_tac |
117 (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, |
117 (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, |
118 div_mult_self_is_m]) 1); |
118 div_mult_self_is_m]) 1); |
119 qed "binomial_Suc_Suc_eq_times"; |
119 qed "binomial_Suc_Suc_eq_times"; |
120 |
120 |