proposition: Lemma iscvg_shift k (u : nat -> R) : iscvg u <-> iscvg (fun n => u (n + k)%N).
proof: Proof. by split=> -[l h]; exists l; apply/(ncvg_shift _ u). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology