more arithmetics for natural numbers with infinity ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_min.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
index 7661dd4868f1acda89640eac5823cf94bfdeecd0..96b8f2a21082ee2103b48d4a402bfaf005397bee 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_min.ma
@@ -20,7 +20,7 @@ fact ymin_pre_dx_aux: ∀x,y. y ≤ x → x - (x - y) ≤ y.
 #x #y * -x -y
 [ #x #y #Hxy >yminus_inj
  /3 width=4 by yle_inj, monotonic_le_minus_l/
-| * // #m >yminus_Y_inj //
+| * //
 ]
 qed-.