lambda_delta: partial commit ...

[helm.git] / matita / matita / contribs / lambda_delta / ground_2 / arith.ma

diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index c51873baa09bb9d8f0c46e2f502e378cb05af921..f7f5e35c4ce10e08a684f7c6f8955530c9899f73 100644 (file)
--- 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 *)