arithmetics for λδ

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

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 16e5bb239708419fbef4c0d6b9574325052a221f..2b3502259f796845194b82ee7d94f64ecca9112a 100644 (file)
--- 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.