X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_pred.ma;h=b64e388773f454ea8e13fc3b7bf131625c323c3f;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=1f14ea6c0c0f57522257d26b43870251eef35322;hpb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;p=helm.git

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 1f14ea6c0..b64e38877 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -12,32 +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).
+interpretation "ynat predecessor" 'DownArrow m = (ypred m).
 
-lemma ypred_O: â«°0 = 0.
+lemma ypred_O: ↓(yinj 0) = yinj 0.
 // qed.
 
-lemma ypred_S: ∀m:nat. ⫰(S m) = m.
+lemma ypred_S: ∀m:nat. ↓(↑m) = yinj m.
 // qed.
 
-lemma ypred_Y: (⫰∞) = ∞.
+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/
+/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
 qed-.