(* *)
(**************************************************************************)
-include "ground_2/notation/functions/predecessor_1.ma".
-include "ground_2/lib/arith.ma".
include "ground_2/ynat/ynat.ma".
(* NATURAL NUMBERS WITH INFINITY ********************************************)
(* 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).
+interpretation "ynat predecessor" 'DownArrow m = (ypred m).
-lemma ypred_O: â«°0 = 0.
+lemma ypred_O: â\86\93(yinj 0) = yinj 0.
// qed.
-lemma ypred_S: â\88\80m:nat. â«°(S m) = m.
+lemma ypred_S: â\88\80m:nat. â\86\93(â\86\91m) = yinj m.
// qed.
-lemma ypred_Y: (â«°∞) = ∞.
+lemma ypred_Y: (â\86\93∞) = ∞.
// 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/
+/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
qed-.