1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/binomial".
17 include "nat/iteration2.ma".
18 include "nat/factorial2.ma".
20 definition bc \def \lambda n,k. n!/(k!*(n-k)!).
22 theorem bc_n_n: \forall n. bc n n = S O.
25 simplify in ⊢ (? ? (? ? (? ? %)) ?).
31 theorem bc_n_O: \forall n. bc n O = S O.
34 simplify in ⊢ (? ? (? ? %) ?).
40 theorem fact_minus: \forall n,k. k < n \to
41 (n-k)*(n - S k)! = (n - k)!.
43 [intro.apply False_ind.
44 apply (lt_to_not_le ? ? H).
54 theorem bc1: \forall n.
55 (\forall i. i < n \to divides (i!*(n-i)!) n!) \to
57 bc (S n) (S k) = (bc n k) + (bc n (S k)).
59 rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
60 [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
61 rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
62 rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
63 [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
64 rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
66 [rewrite < eq_div_plus
67 [rewrite < distr_times_plus.
68 simplify in ⊢ (? ? ? (? (? ? %) ?)).
69 rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
70 rewrite < plus_minus_m_m
71 [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
76 |rewrite > (times_n_O O).
77 apply lt_times;apply lt_O_fact
81 theorem exp_plus_sigma_p:\forall a,b,n.
82 exp (a+b) n = sigma_p (S n) (\lambda k.true)
83 (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
86 |simplify in ⊢ (? ? % ?).
87 rewrite > true_to_sigma_p_Sn