[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / etc / ynat / ynat_plus.etc

lemma pippo: ∀x,y. x + y ≤ x → x = ∞ ∨ y = 0.
/3 width=1 by discr_yplus_xy_x, yle_antisym/ qed-.