- main proposition on lsx finally proved!

[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 596885cf0b55361d538c47008099f3759520aa73..81b9cb01555a38646f10a6882cffa97504d95e55 100644 (file)
--- 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.