proposition: Lemma is_derive_pow (f : R -> R) (n : nat) (x : R) (l : R) : is_derive f x l -> is_derive (fun x : R => (f x)^n) x (INR n * l * (f x)^(pred n)).
proof: Proof. move => H. rewrite (Rmult_comm _ l) Rmult_assoc Rmult_comm. apply is_derive_Reals. apply (derivable_pt_lim_comp f (fun x => x^n)). now apply is_derive_Reals. by apply derivable_pt_lim_pow. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv