proposition: Lemma is_derive_n_scal_r (f : R -> R) (n : nat) (a x l : R) : is_derive_n f n x l -> is_derive_n (fun y => f y * a) n x (l * a).
proof: Proof. move/(is_derive_n_scal_l _ _ a). rewrite Rmult_comm. apply is_derive_n_ext => y ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv