X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_pred.ma;h=1f14ea6c0c0f57522257d26b43870251eef35322;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=652b6e2193365d214fc7484bf2d009c98950dba3;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;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 652b6e219..1f14ea6c0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -26,9 +26,13 @@ definition ypred: ynat → ynat ≝ λm. match m with
 
 interpretation "ynat predecessor" 'Predecessor m = (ypred m).
 
-(* Properties ***************************************************************)
+lemma ypred_O: â«°0 = 0.
+// qed.
+
+lemma ypred_S: ∀m:nat. ⫰(S m) = m.
+// qed.
 
-lemma ypred_inj_rew: ∀m:nat. ⫰m = pred m.
+lemma ypred_Y: (⫰∞) = ∞.
 // qed.
 
 (* Inversion lemmas *********************************************************)