proposition: Lemma continuity_pt_filterlim : forall (f : R -> R) (x : R), continuity_pt f x <-> filterlim f (locally x) (locally (f x)).
proof: Proof. intros f x. eapply iff_trans. apply continuity_pt_locally. apply iff_sym. exact (filterlim_locally f (f x)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub