X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=e51cd799aa11533605db577807b5165ffdd6aff5;hb=723514507b1e2e58c0a8c7bcc39c5d1301b910bc;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..e51cd799a 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.