(* the predecessor function *)
definition ypred: ynat → ynat ≝ λm. match m with
-[ yinj m ⇒ pred m
+[ yinj m ⇒ ⫰m
| Y ⇒ Y
].
interpretation "ynat predecessor" 'Predecessor m = (ypred m).
-(* Properties ***************************************************************)
+lemma ypred_O: ⫰(yinj 0) = yinj 0.
+// qed.
+
+lemma ypred_S: ∀m:nat. ⫰(⫯m) = yinj m.
+// qed.
-lemma ypred_inj_rew: ∀m:nat. ⫰m = pred m.
+lemma ypred_Y: (⫰∞) = ∞.
// qed.
(* Inversion lemmas *********************************************************)
-lemma ypred_inv_refl: ∀m. ⫰m = m → m = 0 ∨ m = ∞.
+lemma ypred_inv_refl: ∀m:ynat. ⫰m = m → m = 0 ∨ m = ∞.
* // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
/4 width=1 by pred_inv_refl, or_introl, eq_f/
qed-.