fact: Definition subset_filter {T} (F : (T -> Prop) -> Prop) (dom : T -> Prop) (P : {x|dom x} -> Prop) : Prop := F (fun x => forall H : dom x, P (exist _ x H)).
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub