+theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
+#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 //
+ ]
+ |#i #_ #_ >(eqb_sym i m) >(eqb_sym i (S m))
+ cases (eqb m i) cases (eqb (S m) i) //
+ |@le_O_n
+ ]
+ |>(eqb_sym (S m) m) >(eq_to_eqb_true ? ? (refl ? (S m)))
+ >(not_eq_to_eqb_false m (S m))
+ [// |@(not_to_not … (not_eq_n_Sn m)) //]
+ |@le_S_S @le_S_S //
+ ]
+ |>(eq_to_eqb_true ?? (refl ? m)) //
+ |@le_S @le_S_S //
+ ]
+ |@lt_sigma_p
+ [//
+ |#i #lti #Hi @le_n
+ |%{0} %
+ [@lt_O_S
+ |%2 %
+ [% // >(not_eq_to_eqb_false 0 (S m)) //
+ >(not_eq_to_eqb_false 0 m) // @lt_to_not_eq //
+ |>bc_n_O <exp_1_n <exp_1_n @le_n
+ ]
+ ]
+ ]
+ ]
+qed.
+