proposition: Lemma filterlim_filter_le_1 : forall {T U F G H} (f : T -> U), filter_le G F -> filterlim f F H -> filterlim 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