X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lt_le_succ.ma;h=56a6dadc9f1f6f759808075c71587f6701861544;hp=73e38daeb4d5648f85521c8e3162f4d0789b4a16;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3

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 73e38daeb..56a6dadc9 100644
--- 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):