proposition: Lemma limit_of_continuous xn x f (yn := Lg Nat (fun i => f (Vg xn i))): BR_seq xn -> continuous_at f x -> limitR xn x -> realp x -> (forall n, natp n -> inc (f (Vg xn n)) BR) -> inc (f x) BR -> (BR_seq yn /\ limitR yn (f x)).
proof: Proof. move => pa pd pe xr pf fxr. have ha: BR_seq yn by apply:BR_seq_prop1. split => // e ep. move: (BQhalf_pos ep)(BQhalf_pos1 ep) => he le0. move/(rlt_cQ (proj31_1 le0) (proj32_1 le0)): le0 => le1. move: (pd _ (RpsS_of_Q he)) => [e1 /BRcompare_zero [d dq dp] h]. move:(pe d dq) => [N NN h2]; exists N => // n nN le2. move: (BR_seq_prop pa nN) (BR_seq_prop ha nN) (pf _ nN) => hb hd hf. have hc: BR_near x e1 (Vg xn n). split => //; rewrite BRabs_diff//; exact:(proj1 (rlt_ltT (h2 _ nN le2) dp)). move: (proj2(h _ hc)); rewrite BRabs_diff // /yn LgV// => le3; apply:(rle_ltT le3 le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)