proposition: Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) -> forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.
proof: Proof. move=> fgh l lfa lga; apply/cvgrPdist_lt => e e_gt0. near=> x; have /(_ _)/andP[//|fg gh] := near fgh x. rewrite distrC ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=. by near: x; apply: (cvgr_lt l); rewrite // ltrDl. by near: x; apply: (cvgr_gt l); rewrite // gtrDl oppr_lt0. 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