proposition: Lemma limit_of_subset2 xn x n (yn:= Lg Nat (fun i => (Vg xn (n +c i)))): limitR yn x -> natp n -> limitR xn x.
proof: Proof. move => pa nN e ep. move:(pa _ ep) => [N NN H]; exists (N +c n); fprops => m mN le. have ha := (NS_diff n mN). move: (Nsum_Mle0 N nN) => hb. move:(cdiff_pr (cleT hb le)) => hc. have hd: N <=c m -c n by apply:(csum_le2l nN NN ha); rewrite hc csumC. by move: (H (m -c n) ha hd); rewrite /yn LgV// hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)