proposition: Lemma cvg_shiftS u_ (l : V) : ([sequence u_ n.+1]_n @ \oo --> l) = (u_ @ \oo --> l).
proof: Proof. suff -> : [sequence u_ n.+1]_n = [sequence u_(n + 1)%N]_n by rewrite cvg_shiftn. by rewrite funeqE => n/=; rewrite addn1. 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