proposition: Lemma ex_derive_scal : forall (f : R -> R) (k x : R), ex_derive f x -> ex_derive (fun x : R => k * f x) x.
proof: Proof. intros f k x (df,Df). exists (k * df). now apply is_derive_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv