equal
deleted
inserted
replaced
48 by (induct n k rule: diff_induct) simp_all |
48 by (induct n k rule: diff_induct) simp_all |
49 |
49 |
50 lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)" |
50 lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)" |
51 apply (safe intro!: binomial_eq_0) |
51 apply (safe intro!: binomial_eq_0) |
52 apply (erule contrapos_pp) |
52 apply (erule contrapos_pp) |
53 apply (simp add: zero_less_binomial) |
53 apply (simp add: neq0_conv zero_less_binomial) |
54 done |
54 done |
55 |
55 |
56 lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)" |
56 lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)" |
57 by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) |
57 by (simp add: neq0_conv linorder_not_less [symmetric] binomial_eq_0_iff [symmetric]) |
58 |
58 |
59 (*Might be more useful if re-oriented*) |
59 (*Might be more useful if re-oriented*) |
60 lemma Suc_times_binomial_eq: |
60 lemma Suc_times_binomial_eq: |
61 "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" |
61 "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" |
62 apply (induct n) |
62 apply (induct n) |