X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Farith.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Farith.ma;h=f7f5e35c4ce10e08a684f7c6f8955530c9899f73;hb=f6464ba2cffc9936b4d8285604786cd91531e0d0;hp=c51873baa09bb9d8f0c46e2f502e378cb05af921;hpb=abed266f42c25bf77c5c4bfbff0450abe9680e7a;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index c51873baa..f7f5e35c4 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -69,6 +69,13 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #Hxy elim (H Hxy)
 qed-.
 
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+#z #x elim x -x normalize
+[ #y <plus_n_Sm #H destruct
+| /3 width=2/
+]
+qed-.
+
 (* iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)