X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_lt_pred.ma;h=2b3502259f796845194b82ee7d94f64ecca9112a;hp=16e5bb239708419fbef4c0d6b9574325052a221f;hb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;hpb=74c6905907b0bca229366d52450e2a6982b5b8be

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
index 16e5bb239..2b3502259 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma
@@ -15,14 +15,14 @@
 include "ground/arith/nat_pred_succ.ma".
 include "ground/arith/nat_lt.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
 
-(* Basic constructions with pred ********************************************)
+(* Constructions with npred *************************************************)
 
 lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m.
 // qed.
 
-(* Basic inversions with pred ***********************************************)
+(* Inversions with npred ****************************************************)
 
 (*** S_pred *)
 lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m.