X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_minus.ma;h=81b9cb01555a38646f10a6882cffa97504d95e55;hb=4e2cde56d7a4c30c1fa07d58f76beab22a174151;hp=596885cf0b55361d538c47008099f3759520aa73;hpb=62af0cd2bf6623bfeacc7d9436e67c39711648a7;p=helm.git

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 596885cf0..81b9cb015 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
@@ -51,6 +51,14 @@ lemma yminus_SO2: ∀m. m - 1 = ⫰m.
 * //
 qed.
 
+lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n.
+* // #n *
+[ #m #Hm #Hn >yminus_inj >yminus_inj
+  /4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/
+| >yminus_Y_inj //
+]
+qed-.
+
 (* Properties on successor **************************************************)
 
 lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.