X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lt_le.ma;h=9c4939f47b8000ad9fda18f1a537d48f6bece3f6;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=84edec50f6725d45c748eb6d8c4e1570fb654935;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
index 84edec50f..9c4939f47 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
@@ -67,7 +67,7 @@ lemma nle_ylt_trans (m) (n) (z):
 
 (* Inversions with yle ******************************************************)
 
-(* ylt_yle_false *)
+(*** ylt_yle_false *)
 lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
 /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.