--- /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 "ground_2/ynat/ynat.ma".
+
+(* INFINITARY NATURAL NUMBERS ***********************************************)
+
+(* the predecessor on ynat *)
+definition ypred: ynat → ynat ≝ λm. match m with
+[ YO ⇒ 0
+| YS n ⇒ n
+].
+
+notation "hvbox( ⫰ term 55 T )"
+ non associative with precedence 55
+ for @{ 'Predecessor $T }.
+
+interpretation "ynat predecessor" 'Predecessor m = (ypred m).
+
+(* Properties ***************************************************************)
+
+lemma ypred_S: ∀m. ⫰⫯m = m.
+// qed.
+
+(* Inversion lemmas *********************************************************)
+
+lemma YS_inj: ∀m,n. ⫯m = ⫯n → m = n.
+#m #n #H <(ypred_S m) <(ypred_S n) //
+qed-.