(* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
definition yplus_aux (x) (n): ynat ≝
- ysucc^n x.
+ (ysucc^n) x.
(*** yplus *)
definition yplus (x): ynat → ynat ≝
(* Basic constructions ******************************************************)
lemma yplus_inj_dx (x) (n):
- ysucc^n x = x + yinj_nat n.
+ (ysucc^n) x = x + yinj_nat n.
#x @(ynat_bind_nat_inj (yplus_aux x))
qed.
(* Constructions with ysucc *************************************************)
(*** yplus_SO2 *)
-lemma yplus_one_dx (x): ↑x = x + 𝟏.
+lemma yplus_unit_dx (x): ↑x = x + 𝟏.
// qed.
(*** yplus_S2 yplus_succ2 *)
<nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
qed.
-(* Advaced constructions ****************************************************)
+(* Advanced constructions ***************************************************)
(*** ysucc_iter_Y yplus_Y1 *)
lemma yplus_inf_sn (x): ∞ = ∞ + x.