(**************************************************************************)
(*       ___                                                              *)
(*      ||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-.