update in ground_2 static_2 basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / etc / lib / arith.etc

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 1af2859d70e14f7e17e5469cbf3a217d3287bab9..11ef739da890ce612a551e5556c118b53b04beac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
@@ -30,3 +30,7 @@ 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-.