rtmap (platform-indepent multple relocation): application and composition

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_pred.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
index 652b6e2193365d214fc7484bf2d009c98950dba3..07fed2a507ba2d1bb940e3dfc7362b5a6748bb92 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -12,28 +12,30 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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).
 
-(* 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-.