proposition: Lemma cvg_at_leftP (f : R -> R) (p l : R) : f x @[x --> p^'-] --> l <-> (forall u : R^nat, (forall n, u n < p) /\ u n @[n --> \oo] --> p -> f (u n) @[n --> \oo] --> l).
proof: Proof. apply: (iff_trans (cvg_at_leftNP f p l)). apply: (iff_trans (cvg_at_rightP _ _ _)). split=> [pfl u [pu up]|pfl u [pu up]]. rewrite -(opprK u); apply: pfl. by split; [move=> k; rewrite ltrNr opprK//|exact/cvgNP]. apply: pfl. by split; [move=> k; rewrite ltrNl//|apply/cvgNP => /=; 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)