proposition: Lemma locally_pt_comp (P : R -> Prop) (f : R -> R) (x : R) : locally (f x) P -> continuity_pt f x -> locally x (fun x => P (f x)).
proof: Proof. intros Lf Cf. apply continuity_pt_filterlim in Cf. now apply Cf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub