#m #x * -m -x
[ #m #n #Hmn #H destruct /3 width=1 by le_n_O_to_eq, eq_f/
| #m #H destruct
-]
+]
qed-.
lemma yle_inv_O2: ∀m:ynat. m ≤ 0 → m = 0.
/3 width=3 by transitive_le, yle_inj/ (**) (* full auto too slow *)
| #x #z #H lapply (yle_inv_Y1 … H) //
]
-qed-.
+qed-.