X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=93fb86d42e0f830e574a0cb685271bc2dc7637d3;hb=472cb969d9a01a6d24eabc39ba20d1dc6adf1b04;hp=203727730e4d2158979e54a986968650f8fcf323;hpb=5117f4af452934db436f22326f35d90f757bdf8a;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 203727730..93fb86d42 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -111,6 +111,9 @@ qed.
 
 (* Inversion & forward lemmas ***********************************************)
 
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
 lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
 /2 width=1 by monotonic_pred/ qed-.
 
@@ -150,6 +153,10 @@ lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
 #H destruct
 qed-.
 
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetics/bigops.ma *)