X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=1ba35c62d31cbe04d1eb1aaae64b044ba64e87e9;hb=325bc2fb36e8f8db99a152037d71332c9ac7eff9;hp=a1b98e180a7fdc101c43999b28223abc3b5a3366;hpb=90293a04a41156a66b381a867714d3563b4c2594;p=helm.git

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index a1b98e180..1ba35c62d 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -163,7 +163,7 @@ op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
 qed.
 
 lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
-#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
+#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c) 
 >associative_plus <plus_minus_m_m //
 qed.
 
@@ -241,7 +241,8 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat →
      >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/
   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
-   #eqi >eqi in ⊢ (???%); >div_plus_times /2 by refl, monotonic_lt_minus_l, trans_eq/ 
+   #eqi >eqi in ⊢ (???%); >div_plus_times 
+   /2 by refl, monotonic_lt_minus_l, trans_eq/ 
   ]
 qed.