X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith_2b.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith_2b.ma;h=c6203acd43af2b0e4a6d95a6bbaeb4ea2821a56e;hb=bac74b5cff042d37e1abc9c961a6c41094b8a294;hp=5729f64cfaa10a3ddd91856cdca539e4e705cb65;hpb=cacd7323994f7621286dbfd93bbf4c50acfbe918;p=helm.git

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 5729f64cf..c6203acd4 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
@@ -42,7 +42,3 @@ 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-.