proposition: Lemma is_lim_Rabs_0 (f : R -> R) (x : Rbar) : is_lim f x 0 -> Rbar_locally' x (fun x => f x <> 0) -> filterlim (fun x => Rabs (f x)) (Rbar_locally' x) (at_right 0).
proof: Proof. intros. eapply filterlim_comp, filterlim_Rabs_0. intros P HP. apply H in HP. generalize (filter_and _ _ H0 HP). rewrite /filtermap /= ; apply filter_imp. intros y Hy. apply Hy, Hy. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis