X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith_2b.ma;h=c6203acd43af2b0e4a6d95a6bbaeb4ea2821a56e;hp=4a1ced64404a1a939f8336e99c5152cc0b35d489;hb=b98ec1a1a37602eca524dc5487c357a200bbb5b6;hpb=eeeaecfafd5ddffa54a41356104fbc60369e5d73

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
index 4a1ced644..c6203acd4 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
@@ -32,8 +32,13 @@ elim (le_or_ge (m11+m12) m21) #Hm1121
 ]
 qed.
 
+lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)).
+// qed.
+
 lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
-* // qed.
+#n1 #n2 <arith_l3 //
+qed.
 
 lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
-// qed.
+#x <arith_l2 //
+qed.