proposition: Lemma continuous_scal_l (f : U -> K) (k : V) (x : U) : continuous f x -> continuous (fun y => scal (f y) k) x.
proof: Proof. intros. apply (continuous_comp f (fun y => scal y k)) => //. apply filterlim_scal_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq