proposition: Lemma ex_derive_n_comp_trans (f : R -> R) (n : nat) (x b : R) : ex_derive_n f n (x + b) -> ex_derive_n (fun y => f (y + b)) n x.
proof: Proof. case: n => [ | n] /= Df. by []. apply ex_derive_ext with (fun x => Derive_n f n (x + b)). simpl => t. apply sym_eq, Derive_n_comp_trans. move: (Derive_n f n) Df => {} f Df. apply ex_derive_comp. apply Df. apply: ex_derive_plus. apply ex_derive_id. apply ex_derive_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv