Final version of the binary machine (all proofs completed).

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma
index b854c356909aef97473e8bc883bc0965517da022..2c47b2873c9ac03f0fcb26b6c5e8192279fe210a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/arith.ma
@@ -80,6 +80,9 @@ qed-.
 lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
 /2 width=4 by le_plus_xySz_x_false/ qed-.
 
+lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
+/2 width=4 by plus_xySz_x_false/ qed-.
+
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)