include "ground/arith/pnat_iter.ma".
-(* POSITIVE INTEGERS ********************************************************)
+(* ADDITION FOR POSITIVE INTEGERS *******************************************)
definition pplus: pnat → pnat → pnat ≝
λp,q. psucc^q p.
interpretation
- "plus (positive integers"
+ "plus (positive integers)"
'plus p q = (pplus p q).
(* Basic rewrites ***********************************************************)
lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
// qed.
-(* Semigroup properties *****************************************************)
+(* Advanced reweites (semigroup properties) *********************************)
lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
#p #q @(piter_appl … psucc)