proposition: Lemma filter_forall : forall {T : Type} {F} {FF: @Filter T F} (P : T -> Prop), (forall x, P x) -> F P.
proof: Proof. intros T F FF P H. apply filter_imp with (fun _ => True). easy. apply filter_true. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub