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 FF dom. constructor. 2: now apply subset_filter_filter. intro H1. unfold subset_filter in H1. specialize (H (fun x : T => dom x -> False)). apply H in H1. apply H1. clear H ; clear H1. intro H2. destruct H2 as (x, Hx). destruct Hx as (Hx1, Hx2) ; now apply Hx2. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub