proposition: Lemma continuity_pt_locally : forall f x, continuity_pt f x <-> forall eps : posreal, locally x (fun u => Rabs (f u - f x) < eps).
proof: Proof. intros f x. split. intros H eps. move: (H eps (cond_pos eps)) => {H} [d [H1 H2]]. rewrite /= /R_dist /D_x /no_cond in H2. exists (mkposreal d H1) => y H. destruct (Req_dec x y) as [<-|Hxy]. rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. by apply H2. intros H eps He. move: (H (mkposreal _ He)) => {H} [d H]. exists d. split. apply cond_pos. intros h [Zh Hh]. exact: H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub