(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_3_2.ma".
include "ground_2/ynat/ynat_lt.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
lemma yplus_succ_swap: ∀m,n. m + ↑n = ↑m + n.
// qed.
-lemma yplus_SO2: ∀m. m + 1 = ↑m.
+lemma yplus_SO2: ∀m:ynat. m + 1 = ↑m.
* //
qed.