proposition: Lemma closed_eq : forall y : R, closed (fun u : R => u = y).
proof: Proof. intros y. apply closed_ext with (fun u => not (u <> y)). intros x. destruct (Req_dec x y) ; intuition. apply closed_not. apply open_neq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub