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