restructuring

[helm.git] / matita / matita / lib / arithmetics / binomial.ma

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index a8b1cef79fad63b88c8e698ce9124e744922d55c..8c5326875f58981e9444e03557deeb36b6d91919 100644 (file)
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/sigma_pi.ma".
 include "arithmetics/primes.ma".
+include "arithmetics/bigops.ma".
 
 (* binomial coefficient *)
 definition bc ≝ λn,k. n!/(k!*(n-k)!).
@@ -23,7 +23,7 @@ theorem bc_n_n: ∀n. bc n n = 1.
 qed.
 
 theorem bc_n_O: ∀n. bc n O = 1.
-#n >bceq <minus_n_O /2/
+#n >bceq <minus_n_O /2 by injective_plus_r/
 qed.
 
 theorem fact_minus: ∀n,k. k < n → 
@@ -68,14 +68,14 @@ theorem bc1: ∀n.∀k. k < n →
 <associative_times in ⊢ (???(?(??%)?));
 >(div_times_times ?? (n - k)) in ⊢ (???(??%)) ; 
   [|>(times_n_O 0) @lt_times // 
-   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
+   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2 by lt_to_le/]
 >associative_times in ⊢ (???(??(??%)));
 >fact_minus // <plus_div 
   [<distributive_times_plus
-   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2 by lt_to_le/] @refl
   |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
   |>associative_times >(commutative_times (S k))
-   <associative_times @divides_times // @bc2 /2/
+   <associative_times @divides_times // @bc2 /2 by lt_to_le/
   |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
   ]
 qed.
@@ -89,13 +89,12 @@ theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
   ]
 qed. 
 
-(*
 theorem binomial_law:∀a,b,n.
-  (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
+  (a+b)^n = ∑_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
 #a #b #n (elim n) //
--n #n #Hind normalize in ⊢ (? ? % ?).
+-n #n #Hind normalize in ⊢ (??%?); >commutative_times
 >bigop_Strue // >Hind >distributive_times_plus 
-<(minus_n_n (S n)) <commutative_times <(commutative_times b)
+<(minus_n_n (S n)) <commutative_times (* <(commutative_times b) *)
 (* hint??? *)
 >(bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b)
 >bigop_Strue in ⊢ (??(??%)?) // <associative_plus 
@@ -120,6 +119,84 @@ theorem exp_S_sigma_p:∀a,n.
 #a #n cut (S a = a + 1) // #H >H
 >binomial_law @same_bigop //
 qed.
+definition M ≝ λm.bc (S(2*m)) m.
+
+theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
+#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
+          ]
+        ]
+      |apply le_S.apply le_S_S.
+       apply le_times_n.
+       apply le_n_Sn
+      |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
+       reflexivity
+      ]
+    |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ? 
+      (\lambda k.bool_to_nat (eqb k m\lor eqb k (S m))*(bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
+     in \vdash (? % ?)
+      [apply lt_sigma_p
+        [intros.elim (eqb i m\lor eqb i (S m))
+          [rewrite > sym_times.rewrite < times_n_SO.apply le_n
+          |apply le_O_n
+          ]
+        |apply (ex_intro ? ? O).
+         split
+          [split[apply lt_O_S|reflexivity]
+          |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)).
+           rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)).
+           simplify in \vdash (? % ?).
+           rewrite < exp_SO_n.rewrite < exp_SO_n.
+           rewrite > bc_n_O.simplify.
+           apply le_n
+          ]
+        ]
+      |intros.rewrite > sym_times in \vdash (? ? ? %).
+       rewrite < times_n_SO.
+       reflexivity
+      ]
+    ]
+  ]
+qed.
+      
 
 (*
 theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).