lift_weight: bug fix

[helm.git] / matita / matita / lib / lambda-delta / ground.ma

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 97c45196a2787917ece829c12fc92c443888fca0..54f9da02a162a1e307e99a4e72ea143c9dbfbe22 100644 (file)
--- 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.