]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_le_lminus.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_lt_le_lminus.ma
index 04e0c4c3c8003ff0442c3bd5035b5531f15e250d..7c7b64f1ab3d6c4d4a3b22cf8f1d0fd38f7c2078 100644 (file)
@@ -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):