proposition: Lemma filterlimi_filter_le_1 : forall {T U F G H} (f : T -> U -> Prop), filter_le G F -> filterlimi f F H -> filterlimi f G H.
proof: Proof. intros T U F G H f K Hf P HP. apply K. now apply Hf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub