X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=3cb9e9f30967ccd92cce8af759037dcc5e22767e;hb=ebc170efe71cf4ee842acfbe58bb6864e76ba98c;hp=d70ea1bfa74cc134edde18bd68c9ffdcc6a9dead;hpb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index d70ea1bfa..3cb9e9f30 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -155,6 +155,9 @@ qed.
 lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
 // qed-.
 
+lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
+/2 width=2 by le_plus_minus_comm/ qed-.
+
 lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
 /2 width=1 by monotonic_pred/ qed-.