proposition: Lemma nlim_lift (u : nat -> R) p : nlim (fun n => u (n + p)%N) = nlim u.
proof: Proof. elim: p => [|p ih]; first by apply/eq_nlim=> k; rewrite addn0. rewrite -ih -[in RHS]nlim_bump; apply/eq_nlim=> k /=. by rewrite addSnnS. 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