proposition: Lemma filterlim_f_0 : filterlim f (at_right 0) (Rbar_locally m_infty).
proof: Proof. unfold f, fab. eapply (filterlim_comp_2 _ _ Rmult). eapply filterlim_comp_2. apply filterlim_const. eapply filterlim_comp_2. apply filterlim_const. by apply is_lim_ln_0. apply (filterlim_Rbar_mult 2 m_infty m_infty). unfold is_Rbar_mult, Rbar_mult'. case: Rle_dec (Rlt_le _ _ Rlt_0_2) => // H _ ; case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Rlt_0_2) => //. apply (filterlim_Rbar_plus 2 _ m_infty). by []. by apply filterlim_Rinv_0_right. by apply (filterlim_Rbar_mult m_infty p_infty). Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)