include "ground_2/ynat/ynat.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* the predecessor function *)
definition ypred: ynat → ynat ≝ λm. match m with
include "ground_2/ynat/ynat.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* the predecessor function *)
definition ypred: ynat → ynat ≝ λm. match m with