proposition: Lemma cvge_at_leftP (f : R -> \bar R) (p l : R) : f x @[x --> p^'-] --> l%:E <-> (forall u : R^nat, (forall n, u n < p) /\ u n @[n --> \oo] --> p -> f (u n) @[n --> \oo] --> l%:E).
proof: Proof. apply: (iff_trans (cvg_at_leftNP f p l%:E)). apply: (iff_trans (cvge_at_rightP _ _ l)); split=> h u [up pu]. - rewrite (_ : u = \- (\- u))%R; last by apply/funext => ?/=; rewrite opprK. by apply: h; split; [by move=> n; rewrite ltrNl opprK|exact: cvgN]. - by apply: h; split => [n|]; [rewrite ltrNl|move/cvgN : pu; rewrite opprK]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)