proposition: Lemma closed_ext : forall D E : T -> Prop, (forall x, D x <-> E x) -> closed D -> closed E.
proof: Proof. intros D E DE CD x Hx. apply DE, CD. contradict Hx. apply: filter_imp Hx. move => {} x Dx Ex. now apply Dx, DE. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub