proposition: Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) : f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l.
proof: Proof. move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0. have {fppl}[a /= a0 fppl] := fppl _ e0; have {fpnl}[b /= b0 fpnl] := fpnl _ e0. near=> t. have : t != p by near: t; exact: nbhs_dnbhs_neq. rewrite neq_lt => /orP[tp|pt]. - apply: fpnl => //=; near: t. exists (b / 2) => //=; first by rewrite divr_gt0. move=> z/= + _ => /lt_le_trans; apply. by rewrite ler_pdivrMr// ler_pMr// ler1n. - apply: fppl =>//=; near: t. exists (a / 2) => //=; first by rewrite divr_gt0. move=> z/= + _ => /lt_le_trans; apply. by rewrite ler_pdivrMr// ler_pMr// ler1n. Unshelve. all: by end_near. 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)