proposition: Lemma f_lim_is_lim alpha beta A (H : 0 < A) (Halpha : (alpha < -1)%Z): filterlim (f alpha beta A) (Rbar_locally p_infty) (locally (f_lim alpha beta A)).
proof: Proof. elim: beta => [ | beta Hbeta]. - rewrite /f /f_lim /Rdiv /Rminus. rewrite -[locally _]/(Rbar_locally (Rbar_mult (Finite _) (Finite _))). rewrite -[filterlim _ _ _]/(is_lim _ p_infty _). apply: is_lim_mult => // . + apply: is_lim_plus. * exact: x_alpha_0. * exact: is_lim_const. * rewrite /is_Rbar_plus /= . by apply f_equal, f_equal, Rplus_0_l. + apply is_lim_const. - rewrite /f /f_lim -/f -/f_lim /Rdiv /Rminus. rewrite -[locally _]/(Rbar_locally (Finite _)). rewrite -[filterlim _ _ _]/(is_lim _ p_infty _). apply: is_lim_plus. + apply: is_lim_mult. * apply: is_lim_plus. - exact: x_alpha_beta. - exact: is_lim_const. - done. * exact: is_lim_const. * done. + apply: is_lim_opp. apply: is_lim_mult. * exact: is_lim_const. * rewrite -[locally _]/(Rbar_locally (Finite _)) in Hbeta. exact Hbeta. * done. + by rewrite Rplus_0_l. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval