X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt.ma;h=a8ffe2e4c6aa27c114e11e684e439a8fb3867725;hb=68e028d053806177e218ee1a5f8778d3011bef83;hp=1df0f857d54d9edc95a70ec09e9cee1e2ddd5298;hpb=74c6905907b0bca229366d52450e2a6982b5b8be;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index 1df0f857d..a8ffe2e4c 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/nat_le.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
 
 (*** lt *)
 definition nlt: relation2 nat nat ≝
@@ -36,26 +36,29 @@ lemma nlt_refl_succ (n): n < ↑n.
 lemma nlt_zero_succ (m): 𝟎 < ↑m.
 /2 width=1 by nle_succ_bi/ qed.
 
+lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
+/2 width=1 by nle_succ_bi/ qed.
+
 (*** le_to_or_lt_eq *)
-lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n.
+lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n.
 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
 qed-.
 
 (*** eq_or_gt *)
-lemma eq_gt_e (n): ∨∨ 𝟎 = n | 𝟎 < n.
-#n elim (nle_lt_eq_e (𝟎) n ?)
+lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n.
+#n elim (nle_lt_eq_dis (𝟎) n ?)
 /2 width=1 by or_introl, or_intror/
 qed-.
 
 (*** lt_or_ge *)
-lemma nlt_ge_e (m) (n): ∨∨ m < n | n ≤ m.
-#m #n elim (nle_ge_e m n) /2 width=1 by or_intror/
-#H elim (nle_lt_eq_e … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
+lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m.
+#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/
+#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
 qed-.
 
 (*** not_le_to_lt *)
 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
-#m #n elim (nlt_ge_e m n) [ // ]
+#m #n elim (nlt_ge_dis m n) [ // ]
 #H #Hn elim Hn -Hn // 
 qed.