proposition: Lemma filterlim_opp : forall x : V, filterlim opp (locally x) (locally (opp x)).
proof: Proof. intros x. rewrite -scal_opp_one. apply filterlim_ext with (2 := filterlim_scal_r _ _). apply: scal_opp_one. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub