some improvements and new lemmas for

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
index 1110f3e44cdd72f41555d45a6c82e80cb99bf234..ef28be4fe5a8a9581ce221715f0acae284136638 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
@@ -35,6 +35,12 @@ lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞.
 #n #IHn >IHn //
 qed.
 
+(* Properties on predecessor ************************************************)
+
+lemma yminus_SO2: ∀m. m - 1 = ⫰m.
+* //
+qed.
+
 (* Properties on successor **************************************************)
 
 lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.