X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_succ.ma;h=a1532adebd035c9ca1ff67af2105d54cc4226ee7;hb=5e72e41f4f86814e56d4b00959ccc56c71042a4c;hp=c93a75d42fc4b9a35b4a93a812633a6291f6f23e;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index c93a75d42..a1532adeb 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/nat.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
 
 definition nsucc: nat → nat ≝ λm. match m with
 [ nzero  ⇒ ninj (𝟏)
@@ -52,7 +52,7 @@ lemma nat_ind_2 (Q:relation2 …):
 #m #IH #n elim n -n /2 width=1 by/
 qed-.
 
-(* Basic inversions *********************************************************)
+(* Basic inversions ***************************************************************)
 
 (*** injective_S *)
 lemma eq_inv_nsucc_bi: injective … nsucc.