proposition: Lemma limit_of_continuous2 xn x f (coerce := fun z => Yo (realp z) z \0r) (yn := Lg Nat (fun i => coerce (f (Vg xn i)))): BR_seq xn -> continuous_at f x -> limitR xn x -> realp x-> inc (f x) BR -> (BR_seq yn /\ limitR yn (f x)).
proof: Proof. move => xns fcx lix xr fxr. have ha: BR_seq yn. apply: BR_seq_prop1 => n nN; rewrite /coerce; Ytac h => //; apply:RS0. split => //. move:(limit_of_continuous_prop xns fcx lix xr)=> [N NN np]. move:(limit_of_subset xns lix NN) => []; set zn := Lg _ _ => zns limz. have hb: forall n, natp n -> realp (f (Vg zn n)). move => n nN; rewrite /zn LgV//; apply: np; fprops;apply:csum_M0le; fprops. move:(proj2 (limit_of_continuous zns fcx limz xr hb fxr)) => l1. have l2:limitR (Lg Nat (fun i => Vg yn (N +c i))) (f x). move => e ep; move:(l1 _ ep) => [M Mn mp]; exists M => // n na nb. move:(NS_sum NN na) => sa;move: (mp _ na nb); rewrite /zn /yn ! LgV//. by rewrite /coerce (Y_true (np (N +c n) sa (Nsum_M0le n NN))). by apply:(limit_of_subset2 l2 NN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)