include "ground_2/ynat/ynat_pred.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* the successor function *)
definition ysucc: ynat → ynat ≝ λm. match m with
include "ground_2/ynat/ynat_pred.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* the successor function *)
definition ysucc: ynat → ynat ≝ λm. match m with
/2 width=2 by ysucc_inv_O_sn/ qed-.
(* Eliminators **************************************************************)
/2 width=2 by ysucc_inv_O_sn/ qed-.
(* Eliminators **************************************************************)