milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
index 694ac940729130980af50518a63e1e9a7f40ab4b..a919727559b6981967a44fc231c964b074f76818 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus.ma
@@ -17,7 +17,7 @@ include "ground/arith/nat_iter.ma".
 (* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
 
 definition nrplus: pnat → nat → pnat ≝
-           λp,n. psucc^n p.
+           λp,n. (psucc^n) p.
 
 interpretation
   "right plus (non-negative integers)"