proposition: Lemma filterlimi_comp : forall T U V (f : T -> U) (g : U -> V -> Prop) F G H, filterlim f F G -> filterlimi g G H -> filterlimi (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 => exists y, g x y /\ P y)). now apply GH. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub