proposition: Lemma ler_cvg_to f g (l l' : R) : f @ a --> l -> g @ a --> l' -> (\near a, f a <= g a) -> l <= l'.
proof: Proof. move=> fl gl; under eq_near do rewrite -subr_ge0; rewrite -subr_ge0. by apply: cvgr_to_ge; apply: cvgB. 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