X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fground.ma;h=23b028eb2a3e99b2c3364d5fa31c2d049963db02;hb=b4d7d16ff7635d9430e92ba86eaf513a9ad9ff8e;hp=72a1eaf294443850b6d0ba2b149e21095f4cf797;hpb=78b1c68fca5f15000588a1e091149a188831977e;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 72a1eaf29..23b028eb2 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 include "basics/list.ma".
+include "lambda-delta/xoa_defs.ma".
+include "lambda-delta/xoa_notation.ma".
 include "lambda-delta/notation.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
@@ -20,7 +22,6 @@ lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 lemma minus_le: ∀m,n. m - n ≤ m.
 /2/ qed.
 
-
 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
 /2/ qed.
 
@@ -29,8 +30,22 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
 >(commutative_plus p) <plus_minus_m_m //
 qed.
 
-lemma lt_false: ∀n. n < n → False.
-#n #H lapply (lt_to_not_eq … H) -H #H elim H -H /2/
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /3/
+qed.
+
+lemma lt_refl_false: ∀n. n < n → False.
+#n #H elim (lt_to_not_eq … H) -H /2/
+qed.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2/
+qed.
+
+lemma plus_lt_false: ∀m,n. m + n < m → False.
+#m #n #H1 lapply (le_plus_n_r n m) #H2
+lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+elim (lt_refl_false … H)
 qed.
 
 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
@@ -44,3 +59,13 @@ lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
 
 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 /2/ qed.
+
+lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
+/2/ qed.
+
+lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
+#m #n #H >minus_plus <minus_minus //
+qed.
+
+lemma arith7: ∀i,d. i ≤ d → d - i + i = d.
+/2/ qed.