- subtraction (and related notions) removed

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc
new file mode 100644 (file)
index 0000000..e535b9f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/ynat/ynat_plus.etc
@@ -0,0 +1,4 @@
+
+lemma pippo: ∀x,y. x + y ≤ x → x = ∞ ∨ y = 0.
+/3 width=1 by discr_yplus_xy_x, yle_antisym/ qed-.
+