proposition: Lemma cvg_shiftn 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_addnr. rewrite -[X in X -> _]cvg_centern; apply: cvg_trans => /=. by apply: near_eq_cvg; near do rewrite subnK; exists N. Unshelve. all: by end_near. 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