update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_lt_le_succ.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
index 73e38daeb4d5648f85521c8e3162f4d0789b4a16..56a6dadc9f1f6f759808075c71587f6701861544 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_succ.ma
@@ -24,7 +24,7 @@ lemma ylt_le_succ_sn (x) (y):
       x < ∞ → ↑x ≤ y → x < y.
 /3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed.
 
-(* Inversions and destructions on yle ***************************************)
+(* Inversions with yle and ysucc ********************************************)
 
 (*** ylt_inv_le *)
 lemma ylt_inv_le_succ_sn (x) (y):