- predefined_virtuals: nwe characters

[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 f7f5e35c4ce10e08a684f7c6f8955530c9899f73..ad3ab4a3d5dab681e6971977d0d3e078251275ec 100644 (file)
--- 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 *)