proposition: Lemma closed_not : forall D : T -> Prop, open D -> closed (fun x => not (D x)).
proof: Proof. intros D OD x Lx Dx. apply Lx. apply: filter_imp (OD _ Dx). intros t Dt nDt. now apply nDt. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub