proposition: Lemma cvg_centern u_ l : ([sequence u_ (n - N)%N]_n @ \oo --> l) = (u_ @ \oo --> l).
proof: Proof. rewrite propeqE; split; last by apply: cvg_comp; apply: cvg_subnr. gen have cD : u_ l / u_ @ \oo --> l -> (fun n => u_ (n + N)%N) @ \oo --> l. by apply: cvg_comp; apply: cvg_addnr. by move=> /cD /=; under [X in X @ _ --> l]funext => n do rewrite addnK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau