proposition: Lemma domin_comp (f : T2 -> U) (g : T2 -> V) (l : T1 -> T2) : filterlim l F G -> is_domin G f g -> is_domin F (fun t => f (l t)) (fun t => g (l t)).
proof: Proof. intros Hl Hg eps. generalize (fun eps => Hl _ (Hg eps)) => {Hl Hg} /= Hl. by apply Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy