-#m #posm @(lt_times_n_to_lt_l 2)
- |change in ⊢ (? ? %) with (exp 2 (S(2*m))).
- change in ⊢ (? ? (? % ?)) with (1+1).
- rewrite > exp_plus_sigma_p.
- apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m)))
- (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
- [rewrite > (sigma_p_gi ? ? m)
- [rewrite > (sigma_p_gi ? ? (S m))
- [rewrite > (false_to_eq_sigma_p O (S(S(2*m))))
- [simplify in ⊢ (? ? (? ? (? ? %))).
- simplify in ⊢ (? % ?).
- rewrite < exp_SO_n.rewrite < exp_SO_n.
- rewrite < exp_SO_n.rewrite < exp_SO_n.
- rewrite < times_n_SO.rewrite < times_n_SO.
- rewrite < times_n_SO.rewrite < times_n_SO.
- apply le_plus
- [unfold M.apply le_n
- |apply le_plus_l.unfold M.
- change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
- simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
- rewrite < plus_n_O.rewrite < minus_plus_m_m.
- rewrite < sym_times in \vdash (? ? (? ? %)).
- change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))).
- simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?).
- rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m).
- rewrite < minus_plus_m_m.
- apply le_n
- ]
- |apply le_O_n
- |intros.
- elim (eqb i m);elim (eqb i (S m));reflexivity
- ]
- |apply le_S_S.apply le_S_S.
- apply le_times_n.
- apply le_n_Sn
- |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
- rewrite > (not_eq_to_eqb_false (S m) m)
- [reflexivity
- |intro.apply (not_eq_n_Sn m).
- apply sym_eq.assumption
+#m #posm @(lt_times_n_to_lt_l 2)
+cut (∀a,b. a^(S b) = a^b*a) [//] #expS <expS
+cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
+>binomial_law
+@(le_to_lt_to_lt ?
+ (∑_{k < S (S (2*m)) | orb (eqb k m) (eqb k (S m))}
+ (bc (S (2*m)) k*1^(S (2*m)-k)*1^k)))
+ [>(bigop_diff ??? plusAC … m)
+ [>(bigop_diff ??? plusAC … (S m))
+ [<(pad_bigop1 … (S(S(2*m))) 0)
+ [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus <Hplus <Hplus
+ whd in ⊢ (? ? (? ? (? ? %)));
+ cut (∀a. 2*a = a + a) [//] #H2a >commutative_times >H2a
+ <exp_1_n <exp_1_n <exp_1_n <exp_1_n
+ <times_n_1 <times_n_1 <times_n_1 <times_n_1
+ @le_plus
+ [@le_n
+ |>Mdef <plus_n_O >bceq >bceq
+ cut (∀a,b.S a - (S b) = a -b) [//] #Hminus >Hminus
+ normalize in ⊢ (??(??(??(?(?%?))))); <plus_n_O <minus_plus_m_m
+ <commutative_times in ⊢ (??(??%));
+ cut (S (2*m)-m = S m)
+ [>H2a >plus_n_Sm >commutative_plus <minus_plus_m_m //]
+ #Hcut >Hcut //