]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_lt_le.ma
index 84edec50f6725d45c748eb6d8c4e1570fb654935..9c4939f47b8000ad9fda18f1a537d48f6bece3f6 100644 (file)
@@ -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-.