proposition: Lemma f0eps_lim_is_lim_sing alpha beta epsilon sing (Halpha : (-1 < alpha)%Z) (Heps : 0 < epsilon) : filterlim (fun x : R => f0eps alpha beta epsilon (/ (x - sing))) (at_right sing) (locally (f0eps_lim alpha beta epsilon)).
proof: Proof. apply: (filterlim_comp _ _ _ (fun x => x - sing) (fun x => f0eps alpha beta epsilon (Rinv x)) _ (at_right 0)). move => P [eps HepsP]. rewrite /filtermap /at_right /within /locally. exists eps => y Hy Hsing. apply: HepsP. have Hepspos : 0 < eps by exact: (cond_pos eps). by apply/ball_to_lra; split; move/ball_to_lra: Hy; lra. lra. exact: f0eps_lim_is_lim. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval