(**************************************************************************)
include "ground/arith/pnat_plus.ma".
+include "ground/arith/nat_pred.ma".
include "ground/arith/nat_rplus_succ.ma".
(* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
p + q = p + ninj q.
// qed.
+lemma nrplus_pnpred_dx (p) (q):
+ pnpred (p+q) = nrplus p (pnpred q).
+#p * //
+qed.
+
lemma nrplus_pplus_assoc (p,q:pnat) (n:nat):
(p+q)+n = p+(q+n).
#p #q #n