--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+
+(* INFINITARY NATURAL NUMBERS ***********************************************)
+
+(* the type of infinitary natural numbers *)
+coinductive ynat: Type[0] ≝
+| YO: ynat
+| YS: ynat → ynat
+.
+
+interpretation "ynat successor" 'Successor m = (YS m).
+
+(* the coercion of nat to ynat *)
+let rec ynat_of_nat n ≝ match n with
+[ O ⇒ YO
+| S m ⇒ YS (ynat_of_nat m)
+].
+
+coercion ynat_of_nat.
+
+(* the infinity *)
+let corec Y : ynat ≝ ⫯Y.
+
+interpretation "ynat infinity" 'Infinity = Y.
+
+(* destructing identity on ynat *)
+definition yid: ynat → ynat ≝ λm. match m with
+[ YO ⇒ 0
+| YS n ⇒ ⫯n
+].
+
+(* Properties ***************************************************************)
+
+fact yid_rew: ∀n. yid n = n.
+* // qed-.
+
+lemma Y_rew: ⫯∞ = ∞.
+<(yid_rew ∞) in ⊢ (???%); //
+qed.