proposition: Lemma open_neq : forall y : R, open (fun u : R => u <> y).
proof: Proof. intros y. apply (open_ext (fun u => u < y \/ y < u)). intros u. split. apply Rlt_dichotomy_converse. apply Rdichotomy. apply open_or. apply open_lt. apply open_gt. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub