proposition: Lemma is_lim_powerRZ_0 alpha (Halpha : (alpha < 0)%Z) : is_lim (powerRZ^~ (alpha)%Z) p_infty (0%R).
proof: Proof. apply: (powerRZ_ind (fun n f => (n < 0)%Z -> is_lim f p_infty (0%R))) => // [n Hn|n Hn|]. - move: Hn. have -> : 0%Z = (Z.of_nat 0%N)%Z by []. rewrite -Nat2Z.inj_lt; lia. - elim: n Hn => [|m Hm Hn] // . rewrite /= . apply: (is_lim_ext_loc (fun x => / x * / x^m)). exists 0 => x Hx. field. split. by apply: pow_nonzero; lra. by lra. case: m Hm Hn => [|m Hm] Hn. + move => _ /=. have -> : 0 = Rbar_mult (Finite 0) (Finite 1) by rewrite /= Rmult_0_l. apply: (is_lim_mult (fun x => / x) (fun x => / 1) p_infty 0 1) => // . exact: is_lim_RInv_p_infty. by rewrite Rinv_1; exact: is_lim_const. have -> : 0 = Rbar_mult (Finite 0) (Finite 0) by rewrite /= Rmult_0_l. apply: (is_lim_mult (fun x => / x) (fun x => / x^m.+1) p_infty 0 0) => // . exact: is_lim_RInv_p_infty. apply: Hm. rewrite Z.opp_neg_pos. have -> : 0%Z = (Z.of_nat 0%N)%Z by []. by rewrite -Nat2Z.inj_lt; lia. move => f g Hfg n H1 H2. apply: (is_lim_ext f g _ _ Hfg). by apply: H1. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval