proposition: Lemma Derive_n_comp_trans (f : R -> R) (n : nat) (x b : R) : Derive_n (fun y => f (y + b)) n x = Derive_n f n (x + b).
proof: Proof. elim: n x => [ | n IH] x /=. by []. rewrite (Derive_ext _ _ _ IH) => {IH}. generalize (Derive_n f n) => {} f. apply (f_equal real). apply Lim_ext => y. replace (x + b + y) with (x + y + b) by ring. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv