proposition: Lemma Derive_scal_l (f : R -> R) (k x : R) : Derive (fun x => f x * k) x = Derive f x * k.
proof: Proof. rewrite Rmult_comm -Derive_scal. apply Derive_ext => t ; by apply Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv