proposition: Lemma cvge_at_rightP (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. split=> [/fine_cvgP [ffin_num fpl] u [pu up]|h]. apply/fine_cvgP; split; last by move/cvg_at_rightP : fpl; exact. have [e /= e0 {}ffin_num] := ffin_num. move/cvgrPdist_lt : up => /(_ _ e0)[s /= s0 {}up]; near=> t. by apply: ffin_num => //=; apply: up => /=; near: t; exists s. suff H : \forall F \near p^'+, f F \is a fin_num. by apply/fine_cvgP; split => //; apply/cvg_at_rightP => u /h /fine_cvgP[]. apply: contrapT => /not_near_at_rightP abs. have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. pose y_ n := sval (cid2 (abs (PosNum (invn n)))). have py_ k : p < y_ k by rewrite /y_ /sval/=; case: cid2 => //= x /andP[]. have y_p : y_ n @[n --> \oo] --> p. apply/cvgrPdist_lt => e e0; near=> t. rewrite ltr0_norm// ?subr_lt0// opprB. rewrite /y_ /sval/=; case: cid2 => //= x /andP[_ + _]. rewrite ltrBlDr => /lt_le_trans; apply. rewrite addrC lerD2r -(invrK e) lef_pV2// ?posrE ?invr_gt0//. near: t. exists `|ceil e^-1|%N => // k /= ek. rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//. by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW. by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW. have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). near \oo => n. have mn : (m <= n)%N by near: n; exists m. have {mn} := mfy_ _ mn. rewrite /y_ /sval; case: cid2 => /= x _. 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)