proposition: Lemma filterlim_Ropp_left (x : R) : filterlim Ropp (at_left x) (at_right (- x)).
proof: Proof. move => P [d /= Hd]. exists d => y /= Hy Hy'. apply Hd. rewrite /ball /= /AbsRing_ball /abs /minus /plus /opp /=. rewrite -Ropp_plus_distr Rabs_Ropp. by apply Hy. by apply Ropp_lt_contravar. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq