proposition: Lemma is_lim_pow_0 (f : R -> R) n : is_lim f p_infty 0 -> is_lim (fun x => (f x)^n.+1) p_infty 0.
proof: Proof. elim: n => [|n Hn]. - apply: (is_lim_ext f) => // . by move => y; rewrite pow_1. - move => Hf0. apply: (is_lim_ext (fun x => (f x) * (f x)^n.+1)). by move => y. have {1}-> : 0 = Rbar_mult 0 0 by rewrite /= Rmult_0_l. apply: (is_lim_mult f (fun x => (f x)^n.+1) p_infty 0 0) => // . exact: Hn. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval