proposition: Lemma nlim_bump (u : nat -> R) : nlim (fun n => u n.+1) = nlim u.
proof: Proof. case: (nlimP u) => [l cu|Ncu]. suff: ncvg (fun n => u n.+1) l by move/nlimE. move=> v; case/(_ v): cu => K cu; exists K => n le_Kn. by apply/cu; apply/(leq_trans le_Kn). rewrite nlim_out //; case=> l cu; apply/Ncu; exists l. move=> v; case/(_ v): cu => K cu; exists K.+1 => n le_Kn. rewrite -[n]prednK; first by apply/(leq_trans _ le_Kn). by apply/cu; rewrite -ltnS prednK ?(leq_trans _ le_Kn). 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