X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus_rplus.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus_rplus.ma;h=b799fc15df8d94f93071fc47ffa2637ecb94021c;hb=2ed8d2abcc3b0687141b627061b63350a0b200bd;hp=e80e2414f73a3a905453f61ab38eec311d5dd47c;hpb=b367de0252e88d6b0476648d5ceac7e4aeffca27;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
index e80e2414f..b799fc15d 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_rplus.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_plus.ma".
 
 (* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
 
-(* Constructions with rplus *************************************************)
+(* Constructions with nrplus ************************************************)
 
 lemma nrplus_inj_sn (p) (n):
       ninj (p + n) = ninj p + n.
@@ -25,7 +25,7 @@ lemma nrplus_inj_sn (p) (n):
 #n #IH <nplus_succ_dx <IH //
 qed.
 
-(* Constructions with rplus and npsucc **************************************)
+(* Constructions with nrplus and npsucc *************************************)
 
 lemma nrplus_npsucc_sn (m) (n):
       npsucc (m + n) = npsucc m + n.