X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=6bcd62a653b38465021da0bb395700089e4afd70;hb=7da6488b45e5dfc1b675552a7f19c58a6abbff2b;hp=03db53f7d5ff0f9863abaeba9cfe10f5bd681a33;hpb=7ad16d18416a08382d62747fce4a0ac18ee557e0;p=helm.git

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 03db53f7d..6bcd62a65 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -192,7 +192,7 @@ op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
 #k #p #B #nil #op #f #g (elim k) [normalize @nill]
 -k #k #Hind (cases (true_or_false (p k))) #H
   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
-   <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
+   normalize <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
    <assoc @eq_f @Hind
   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
   ]
@@ -209,7 +209,7 @@ lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
       [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
      cases (true_or_false (p n)) #pn 
       [>bigop_Strue // >bigop_Strue //
-       >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
+       normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
       |>bigop_Sfalse // >bigop_Sfalse // >Hind //  
       ]
     |<Hi >bigop_Strue // @eq_f >bigop_Sfalse