proposition: Lemma filter_const : forall {T : Type} {F} {FF: @ProperFilter T F} (P : Prop), F (fun _ => P) -> P.
proof: Proof. intros T F FF P H. destruct (filter_ex (fun _ => P) H) as [_ H']. exact H'. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub