proposition: Lemma is_derive_n_comp_scal (f : R -> R) (a : R) (n : nat) (x l : R) : locally (a * x) (fun x => forall k, (k <= n)%nat -> ex_derive_n f k x) -> is_derive_n f n (a * x) l -> is_derive_n (fun y => f (a * y)) n x (a ^ n * l).
proof: Proof. case: n => /= [ | n] Hfn Hf. by rewrite Rmult_1_l. apply is_derive_unique in Hf. rewrite -Hf. rewrite -(Derive_n_comp_scal f a (S n) x) => //. apply Derive_correct. by apply (ex_derive_n_comp_scal f a (S n) x). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv