-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/