X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_minus.ma;h=81b9cb01555a38646f10a6882cffa97504d95e55;hb=14a8276e6d877c2281a1fda452ed3e4c150f5d39;hp=1110f3e44cdd72f41555d45a6c82e80cb99bf234;hpb=114ab6653242120dca8382327447ac24cb255f42;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 1110f3e44..81b9cb015 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_minus.ma
@@ -35,12 +35,48 @@ lemma yminus_Y_inj: ∀n. ∞ - yinj n = ∞.
 #n #IHn >IHn //
 qed.
 
+lemma yminus_O1: ∀x:ynat. 0 - x = 0.
+* // qed.
+
+lemma yminus_refl: ∀x:ynat. x - x = 0.
+* // qed.
+
+lemma yminus_minus_comm: ∀y,z,x. x - y - z = x - z - y.
+* #y [ * #z [ * // ] ] >yminus_O1 //
+qed.
+
+(* Properties on predecessor ************************************************)
+
+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.
 * // #n * [2: >yminus_Y_inj // ]
 #m >yminus_inj //
-qed. 
+qed.
+
+lemma yminus_succ1_inj: ∀n:nat. ∀m:ynat. n ≤ m → ⫯m - n = ⫯(m - n).
+#n *
+[ #m #Hmn >yminus_inj >yminus_inj
+  /4 width=1 by yle_inv_inj, plus_minus, eq_f/
+| >yminus_Y_inj //
+]
+qed-.
+
+lemma yminus_succ2: ∀y,x. x - ⫯y = ⫰(x-y).
+* //
+qed.
 
 (* Properties on order ******************************************************)
 
@@ -59,3 +95,15 @@ lemma yminus_to_le: ∀n:ynat. ∀m:ynat. m - n = 0 → m ≤ n.
 | >yminus_Y_inj #H destruct
 ]
 qed.
+
+lemma monotonic_yle_minus_dx: ∀x,y. x ≤ y → ∀z. x - z ≤ y - z.
+#x #y #Hxy * //
+#z elim z -z /3 width=1 by yle_pred/
+qed.
+
+(* Properties on strict order ***********************************************)
+
+lemma monotonic_ylt_minus_dx: ∀x,y:ynat. x < y → ∀z:nat. z ≤ x → x - z < y - z.
+#x #y * -x -y
+/4 width=1 by ylt_inj, yle_inv_inj, monotonic_lt_minus_l/
+qed.