X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus_rplus.ma;h=b799fc15df8d94f93071fc47ffa2637ecb94021c;hb=9605ffc88831066a901ea4eb8e419f277662f372;hp=e80e2414f73a3a905453f61ab38eec311d5dd47c;hpb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;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.