proposition: Lemma squeeze_cvge f g h : (\near a, f a <= g a <= h a) -> forall (l : \bar R), f @ a --> l -> h @ a --> l -> g @ a --> l.
proof: Proof. move=> fgh [l||]; last 2 first. - by move=> + _; apply: gee_cvgy; apply: filterS fgh => ? /andP[]. - by move=> _; apply: lee_cvgNy; apply: filterS fgh => ? /andP[]. move=> /fine_cvgP[Ff fl] /fine_cvgP[Fh hl]; apply/fine_cvgP. have Fg := squeeze_fin fgh Ff Fh; split=> //. apply: squeeze_cvgr fl hl; near=> x => /=. by have /(_ _)/andP[//|fg gh] := near fgh x; rewrite !fine_le//=; near: x. 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