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