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.ma;h=7c7b64f1ab3d6c4d4a3b22cf8f1d0fd38f7c2078;hp=04e0c4c3c8003ff0442c3bd5035b5531f15e250d;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
index 04e0c4c3c..7c7b64f1a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_lt.ma".
 
 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
 
-(* Cobstructions with yle and ylminus  **************************************)
+(* Constructions with yle and ylminus ***************************************)
 
 (*** monotonic_ylt_minus_dx *)
 lemma ylt_lminus_bi_dx (o) (x) (y):