proposition: Lemma filterlim_Rabs (x : Rbar) : filterlim Rabs (Rbar_locally' x) (Rbar_locally (Rbar_abs x)).
proof: Proof. destruct x as [x| | ] => //=. eapply filterlim_filter_le_1, continuous_Rabs. intros P [d HP] ; exists d => y Hy _. by apply HP. eapply filterlim_ext_loc. exists 0 => y Hy. rewrite Rabs_pos_eq // ; by apply Rlt_le. apply is_lim_id. eapply filterlim_ext_loc. exists 0 => y Hy. rewrite -Rabs_Ropp Rabs_pos_eq // -Ropp_0 ; by apply Ropp_le_contravar, Rlt_le. apply (is_lim_opp id m_infty m_infty), is_lim_id. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis