proposition: Lemma filterlim_abs_0 {K : AbsRing} : (forall x : K, abs x = 0 -> x = zero) -> filterlim (abs (K := K)) (locally' (zero (G := K))) (at_right 0).
proof: Proof. intros H P [eps HP]. exists eps. intros x Hx Hx'. apply HP. revert Hx. rewrite /ball /= /AbsRing_ball !minus_zero_r {2}/abs /= Rabs_pos_eq. by []. by apply abs_ge_0. assert (abs x <> 0). contradict Hx' ; by apply H. case: (abs_ge_0 x) => // H1. by rewrite -H1 in H0. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis