proposition: Lemma filterlim_Rabs_0 : filterlim Rabs (Rbar_locally' 0) (at_right 0).
proof: Proof. apply @filterlim_abs_0. by apply Rabs_eq_0. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis