proposition: Lemma ex_derive_scal_l : forall (f : K -> K) (x : K) (k : V), ex_derive f x -> ex_derive (fun x => scal (f x) k) x.
proof: Proof. intros f x k [df Df]. exists (scal df k). by apply is_derive_scal_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv