arithmetics for λδ

[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..05776ef200767e8371a9721435b19cd8683ee7ea 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.
@@ -35,7 +35,7 @@ qed.
 lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n.
 /2 width=1/ qed-.
 
-(* Basic inversions with plus ***********************************************)
+(* Inversions with nplus ****************************************************)
 
 (*** lt_plus_to_lt_l *)
 lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2.