update in ground

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

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 6a66bded3d53f813a9aab4ab7b86a19dcb2edbcc..c39589b9986a5f00cdb245c9a4d5a64e734e307a 100644 (file)
--- 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):