proposition: Lemma ncvg_shift k (u : nat -> R) l : ncvg u l <-> ncvg (fun n => u (n + k)%N) l.
proof: Proof. split => h v; move/(_ v): h => [K h]. + by exists K => n leKn; apply/h/(leq_trans leKn)/leq_addr. + exists (K + k)%N => n leKkn; rewrite -[n](@subnK k). * by apply/(leq_trans _ leKkn)/leq_addl. apply/h/(@leq_trans ((K+k) - k))/leq_sub2r => //. by rewrite addnK. 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