proposition: Lemma cvg_at_rightP (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. split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt ucvg]|pfl]. apply/cvgrPdist_le => e e0. have [r /= r0 {}fpl] := fpl _ e0; have [s /= s0 {}ucvg] := ucvg _ r0. near=> t; apply: fpl => //=; apply: ucvg => /=. by near: t; exists s. apply: contrapT => fpl; move: pfl; apply/existsNP. suff: exists2 x : R ^nat, (forall k, x k > p) /\ x n @[n --> \oo] --> p & ~ f (x n) @[n --> \oo] --> l. by move=> [x_] h; exists x_; exact/not_implyP. have [e He] : exists e : {posnum R}, forall d : {posnum R}, exists xn : R, [/\ xn > p, `|xn - p| < d%:num & `|f xn - l| >= e%:num]. apply: contrapT; apply: contra_not fpl => /forallNP h. apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0). move/forallNP => {}h; near=> t. have /not_and3P[abs|abs|/negP] := h t. - by exfalso; apply: abs; near: t; exact: nbhs_right_gt. - exfalso; apply: abs. by near: t; by exists d%:num => //= z/=; rewrite distrC. - by rewrite -ltNge distrC => /ltW. have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. exists (fun n => sval (cid (He (PosNum (invn n))))). split => [k|]; first by rewrite /sval/=; case: cid => x []. apply/cvgrPdist_lt => r r0; near=> t. rewrite /sval/=; case: cid => x [px xpt _]. rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//. near: t; exists `|ceil (r^-1)|%N => // s /=. rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans. by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge. move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). rewrite /sval/=; case: cid => // x [px xpn]. by rewrite leNgt distrC => /negP. 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)