X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lt_plus.ma;h=06e7d081326ffecc2b5f2b3e3a870271888a9f41;hp=8f8ecd3aa07322142f444cdb9a90192285137a09;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
index 8f8ecd3aa..06e7d0813 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_plus.ma
@@ -88,7 +88,7 @@ lemma yplus_inv_plus_bi_23 (z) (x1) (x2) (y1) (y2):
       z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
 #z #x1 #x2 #y1 #y2 #Hz
 <yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
-@(eq_inv_yplus_bi_dx … H) // (**) (* auto does not work *)
+@(eq_inv_yplus_bi_dx … H) // (* * auto does not work *)
 qed-.
 
 (*** ylt_inv_plus_Y *)