proposition: Lemma closed_and : forall D E : T -> Prop, closed D -> closed E -> closed (fun x => D x /\ E x).
proof: Proof. intros D E CD CE x Hx. split. apply CD. contradict Hx. apply: filter_imp Hx. move => {} x nDx [Dx _]. now apply nDx. apply CE. contradict Hx. apply: filter_imp Hx. move => {} x nEx [_ Ex]. now apply nEx. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub