proposition: Lemma lee_cvg_to f g l l' : f @ a --> l -> g @ a --> l' -> (\near a, f a <= g a) -> l <= l'.
proof: Proof. move=> + + fg; move: l' l. move=> /= [l'||] [l||]//=; rewrite ?leNye ?leey//=; first 1 last. - by move=> /(gee_cvgy fg) /cvg_lim<-// /cvg_lim<-. - by move=> /cvg_lim <-// /(lee_cvgNy fg) /cvg_lim<-. - by move=> /(gee_cvgy fg) /cvg_lim<-// /cvg_lim<-. move=> /fine_cvgP[Ff fl] /fine_cvgP[Fg gl]. rewrite lee_fin -(cvg_lim _ fl)// -(cvg_lim _ gl)//. by apply: ler_lim; [apply: cvgP fl|apply: cvgP gl|near do apply: fine_le]. Unshelve. all: end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule