proposition: Lemma filter_le_within : forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} D, filter_le (within D F) F.
proof: Proof. intros T F D P HP. unfold within. now apply filter_imp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub