proposition: Lemma limit_of_continuous_prop xn x f: BR_seq xn -> continuous_at f x -> limitR xn x -> realp x -> exists2 N, natp N & forall n, natp n -> N <=c n -> realp (f (Vg xn n)).
proof: Proof. move => ha pd pe xr. move:(pd _ RpsS1) => [d /BRcompare_zero [d1 dq dp] h]. move:(pe _ dq) => [N NN Np]; exists N => // n na nb. have xnn: realp (Vg xn n) by apply: BR_seq_prop. move:(Np _ na nb)=> hh. have:BR_near x d (Vg xn n). split => //; rewrite BRabs_diff //; exact (proj1(rlt_ltT hh dp)). by move/h => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)