(* 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):