nth_current_chars

[helm.git] / matita / matita / lib / arithmetics / bigops.ma

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index a1b98e180a7fdc101c43999b28223abc3b5a3366..e51cd799aa11533605db577807b5165ffdd6aff5 100644 (file)
--- 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.