proposition: Lemma subset_filter_proper : forall {T F} {FF : Filter F} (dom : T -> Prop), (forall P, F P -> exists x, dom x /\ P x) -> ProperFilter (subset_filter F dom).
proof: Proof. intros T F dom FF H. constructor. - unfold subset_filter. intros P HP. destruct (H _ HP) as [x [H1 H2]]. exists (exist _ x H1). now apply H2. - now apply subset_filter_filter. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub