X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Farith.ma;h=ad3ab4a3d5dab681e6971977d0d3e078251275ec;hb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;hp=f7f5e35c4ce10e08a684f7c6f8955530c9899f73;hpb=f6464ba2cffc9936b4d8285604786cd91531e0d0;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 f7f5e35c4..ad3ab4a3d 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -69,13 +69,17 @@ 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/
+lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
+#y #z #x elim x -x
+[ #H lapply (le_n_O_to_eq … H) -H
+  <plus_n_Sm #H destruct
+| /3 width=1 by le_S_S_to_le/
 ]
 qed-.
 
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+/2 width=4 by le_plus_xySz_x_false/ qed-.
+
 (* iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)