- inversion lemmas for tpr completed!

[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 d39b3faf46667050c302cd13a535595b9e383a21..54f9da02a162a1e307e99a4e72ea143c9dbfbe22 100644 (file)
--- 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.