X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fetc%2Flib%2Farith.etc;h=11ef739da890ce612a551e5556c118b53b04beac;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=656a4425577d9810533248ed264f2630981cc9a6;hpb=e500cfb0c28718d44972a119f55f152018d18e62;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
index 656a44255..11ef739da 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
@@ -16,3 +16,21 @@ qed-.
 lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
 #x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
 qed-.
+
+lemma lt_dec: ∀n2,n1. Decidable (n1 < n2).
+#n2 elim n2 -n2
+[ /4 width=3 by or_intror, absurd, nmk/
+| #n2 #IHn2 * /2 width=1 by or_introl/
+  #n1 elim (IHn2 n1) -IHn2
+  /4 width=1 by le_S_S, monotonic_pred, or_intror, or_introl/
+]
+qed-.
+
+lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
+#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
+#Hxy elim (H Hxy)
+qed-.
+
+lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
+#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
+qed-.