proposition: Lemma f_lim_correct alpha beta A (H : 0 < A) (Halpha : (alpha < -1)%Z) : Bertrand_lim alpha beta A (f_lim alpha beta A).
proof: Proof. rewrite /Bertrand_lim. apply prodi_to_single_l. apply: (filterlimi_lim_ext_loc (f alpha beta A)). exists A => x Hx. apply f_correct. apply (conj H). exact: Rlt_le. exact: Zlt_not_eq. exact: f_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