proposition: Lemma continuous_comp {U V W : UniformSpace} (f : U -> V) (g : V -> W) (x : U) : continuous f x -> continuous g (f x) -> continuous (fun x => g (f x)) x.
proof: Proof. by apply filterlim_comp. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq