propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_lt_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
index e9920e928dc2941d58e48f4a359f548d94023296..0f0a21c829a551516ca199498b200384e5c32eab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma
@@ -15,9 +15,9 @@
 include "ground/arith/nat_le_plus.ma".
 include "ground/arith/nat_lt.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
 
-(* Basic constructions with plus ********************************************)
+(* Constructions with nplus *************************************************)
 
 (*** monotonic_lt_plus_l *)
 lemma nlt_plus_bi_dx (m) (n1) (n2): n1 < n2 → n1 + m < n2 + m.
@@ -31,11 +31,16 @@ lemma nlt_plus_bi_sn (m) (n1) (n2): n1 < n2 → m + n1 < m + n2.
 @nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/
 qed.
 
-(*** lt_plus_Sn_r *) (**)
-lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
-/2 width=1/ qed-.
+lemma nlt_plus_dx_dx (o) (m) (n): m < n → m < n + o.
+/2 width=1 by nle_plus_dx_dx/ qed.
 
-(* Basic inversions with plus ***********************************************)
+lemma nlt_plus_dx_sn (o) (m) (n) : m < n → m < o + n.
+/2 width=1 by nle_plus_dx_sn/ qed.
+
+lemma nlt_succ_plus_dx_refl_sn (m) (n): m < ↑(m + n).
+/2 width=1/ qed.
+
+(* Inversions with nplus ****************************************************)
 
 (*** lt_plus_to_lt_l *)
 lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2.