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_lminus_plus.ma;h=c39589b9986a5f00cdb245c9a4d5a64e734e307a;hp=6a66bded3d53f813a9aab4ab7b86a19dcb2edbcc;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
index 6a66bded3..c39589b99 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus_plus.ma
@@ -17,7 +17,7 @@ include "ground/arith/ynat_lt_le_lminus.ma".
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 
-(* Constructions with yle and ylminus and yplus  ****************************)
+(* Constructions with yle and ylminus and yplus *****************************)
 
 (*** ylt_plus2_to_minus_inj2 *)
 lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y):