proposition: Lemma limit_of_subset xn x n (yn:= Lg Nat (fun i => (Vg xn (n +c i)))): BR_seq xn -> limitR xn x -> natp n -> (BR_seq yn /\ limitR yn x).
proof: Proof. move => pa pb nN. have ha: BR_seq yn. apply: BR_seq_prop1. by move => k kn;apply: BR_seq_prop => //;apply:NS_sum. split =>// e ep;move:(pb _ ep) => [N NN H]; exists N => // m mN le. rewrite /yn LgV//; apply: H; fprops. apply (cleT le); apply:csum_Mle0; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)