X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;fp=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;h=54f9da02a162a1e307e99a4e72ea143c9dbfbe22;hb=d1c48262d83ff5917fe5ad0d5cbbed8d686c046a;hp=d39b3faf46667050c302cd13a535595b9e383a21;hpb=dd88a8fa58d50833118cadd96ba8e3bcf70340a4;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index d39b3faf4..54f9da02a 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -21,6 +21,12 @@ lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
 // qed.
 
+lemma arith8: ∀a,b. a < a + b + 1.
+// qed.
+
+lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
+// qed.
+
 lemma minus_le: ∀m,n. m - n ≤ m.
 /2/ qed.