X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;h=54f9da02a162a1e307e99a4e72ea143c9dbfbe22;hb=dde568d876a5d2e1b6e554a526c98b09b145d25a;hp=97c45196a2787917ece829c12fc92c443888fca0;hpb=00cafb21b9177a6c48e51e97ba13aa1baad2c1b1;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 97c45196a..54f9da02a 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -12,7 +12,6 @@
 include "basics/list.ma".
 include "lambda-delta/xoa_defs.ma".
 include "lambda-delta/xoa_notation.ma".
-include "lambda-delta/notation.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
@@ -22,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.