proposition: Lemma open_not : forall D : T -> Prop, closed D -> open (fun x => not (D x)).
proof: Proof. intros D CD x Dx. apply locally_not. intros H. apply Dx, CD. intros [eps He]. now apply (H eps). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub