proposition: Lemma continuous_scal (k : U -> K) (f : U -> V) (x : U) : continuous k x -> continuous f x -> continuous (fun y => scal (k y) (f y)) x.
proof: Proof. intros. by eapply filterlim_comp_2, filterlim_scal. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq