proposition: Theorem continuity_pt_ne : forall f x y, f x <> y -> continuity_pt f x -> locally_true x (fun u => f u <> y).
proof: Proof. intros. destruct (Rdichotomy _ _ H) as [H1|H1]. destruct (continuity_pt_lt _ _ _ H1 H0) as (delta, (Hdelta, H2)). exists delta. split. exact Hdelta. intros. apply Rlt_not_eq. exact (H2 _ H3). destruct (continuity_pt_gt _ _ _ H1 H0) as (delta, (Hdelta, H2)). exists delta. split. exact Hdelta. intros. apply Rgt_not_eq. exact (H2 _ H3). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)