proposition: Lemma filterlim_comp : forall T U V (f : T -> U) (g : U -> V) F G H, filterlim f F G -> filterlim g G H -> filterlim (fun x => g (f x)) F H.
proof: Proof. intros T U V f g F G H FG GH P HP. apply (FG (fun x => P (g x))). now apply GH. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub