proposition: Lemma lime_sup_inf_at_right f a l : lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'+] --> l%:E.
proof: Proof. move=> supfpl inffpl; apply/cvge_at_rightP => u [pu up]. have fu : \forall n \near \oo, f (u n) \is a fin_num. have [dsup Hdsup] := lime_supP supfpl (PosNum ltr01). have [dinf Hdinf] := lime_infP inffpl (PosNum ltr01). near=> n; rewrite fin_numE; apply/andP; split. apply/eqP => fxnoo. suff : (ball a dinf%:num `\ a) (u n) by move=> /Hdinf; rewrite fxnoo. split; last by apply/eqP; rewrite gt_eqF. by near: n; move/cvgrPdist_lt : up; exact. apply/eqP => fxnoo. suff : (ball a dsup%:num `\ a) (u n) by move=> /Hdsup; rewrite fxnoo. split; last by apply/eqP; rewrite gt_eqF. by near: n; move/cvgrPdist_lt : up; exact. apply/fine_cvgP; split => /=; first exact: fu. apply/cvgrPdist_le => _/posnumP[e]. have [d1 Hd1] : exists d1 : {posnum R}, l%:E - e%:num%:E <= ereal_inf [set f x | x in ball a d1%:num `\ a]. have : l%:E - e%:num%:E < lime_inf f a. by rewrite inffpl lte_subl_addr// lteDl. rewrite lime_infE => /ereal_sup_gt[x /= [r]]; rewrite in_itv/= andbT. move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW//. by rewrite -inf_ballE. have [d2 Hd2] : exists d2 : {posnum R}, ereal_sup [set f x | x in ball a d2%:num `\ a] <= l%:E + e%:num%:E. have : lime_sup f a < l%:E + e%:num%:E by rewrite supfpl lteDl. rewrite lime_supE => /ereal_inf_lt[x /= [r]]; rewrite in_itv/= andbT. by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW. pose d := minr d1%:num d2%:num. have d0 : (0 < d)%R by rewrite lt_minr; apply/andP; split => //=. move/cvgrPdist_lt : up => /(_ _ d0)[m _] {}ucvg. near=> n. rewrite /= ler_distlC; apply/andP; split. rewrite -lee_fin EFinB (le_trans Hd1)//. rewrite (@le_trans _ _ (ereal_inf [set f x | x in ball a d `\ a]))//. apply: le_ereal_inf => _/= [r [adr ra] <-]; exists r => //; split => //. by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx. apply: ereal_inf_lb => /=; exists (u n). split; last by apply/eqP; rewrite eq_sym lt_eqF. by apply: ucvg => //=; near: n; by exists m. by rewrite fineK//; by near: n. rewrite -lee_fin EFinD (le_trans _ Hd2)//. rewrite (@le_trans _ _ (ereal_sup [set f x | x in ball a d `\ a]))//; last first. apply: le_ereal_sup => z/= [r [adr rp] <-{z}]; exists r => //; split => //. by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx orbT. apply: ereal_sup_ub => /=; exists (u n). split; last by apply/eqP; rewrite eq_sym lt_eqF. by apply: ucvg => //=; near: n; exists m. by rewrite fineK//; near: n. 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)