milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith_2b.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
index c6203acd43af2b0e4a6d95a6bbaeb4ea2821a56e..5729f64cfaa10a3ddd91856cdca539e4e705cb65 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
@@ -42,3 +42,7 @@ qed.
 lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
 #x <arith_l2 //
 qed.
+
+lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
+#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
+qed-.