proposition: Lemma filterlim_Rbar_opp : forall x, filterlim Ropp (Rbar_locally x) (Rbar_locally (Rbar_opp x)).
proof: Proof. intros [x| |] P [eps He]. - exists eps. intros y Hy. apply He. rewrite /ball /= /AbsRing_ball /abs /minus /plus /opp /=. by rewrite Ropp_involutive Rplus_comm Rabs_minus_sym. - exists (-eps). intros y Hy. apply He. apply Ropp_lt_cancel. by rewrite Ropp_involutive. - exists (-eps). intros y Hy. apply He. apply Ropp_lt_cancel. by rewrite Ropp_involutive. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy