X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbinomial.ma;h=6b4d3ff52764ff41ee26453c9c26c6206c2ab7b3;hb=74223db3fc45caccb3cfac80971b29cb0613da28;hp=c3834c8d847b8d001f48ef19217b9d121e1a2944;hpb=342278d86d2ebb11b046dcc9f44cc5d08cd16352;p=helm.git

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index c3834c8d8..6b4d3ff52 100644
--- 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 //