update in basic_2

[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 74d2c8efd5ad9ecda487fe89cd5e618d50cc3fbb..6b4d3ff52764ff41ee26453c9c26c6206c2ab7b3 100644 (file)
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -103,7 +103,7 @@ theorem binomial_law:∀a,b,n.
 >bigop_Strue in ⊢ (??(??%)?); // <associative_plus 
 <commutative_plus in ⊢ (??(? % ?) ?); >associative_plus @eq_f2
   [<minus_n_n >bc_n_n >bc_n_n normalize //
-  |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?);
+  |>(bigop_0 ??? plusA)  >associative_plus >commutative_plus in ⊢ (??(??%)?);
    <associative_plus >(bigop_0 n ?? plusA) @eq_f2 
     [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus >Hplus 
      >(bigop_op n ??? plusAC) @same_bigop //
@@ -191,13 +191,3 @@ cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
   ]
 qed.
       
-(*
-theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
-intros.simplify.
-rewrite < times_n_SO.
-rewrite < plus_n_O.
-rewrite < sym_times.simplify.
-rewrite < assoc_plus.
-rewrite < sym_plus.
-reflexivity.
-qed. *)