update in ground

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

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 e80e2414f73a3a905453f61ab38eec311d5dd47c..b799fc15df8d94f93071fc47ffa2637ecb94021c 100644 (file)
--- 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.