proposition: Lemma is_derive_n_comp_trans (f : R -> R) (n : nat) (x b l : R) : is_derive_n f n (x + b) l -> is_derive_n (fun y => f (y + b)) n x l.
proof: Proof. case: n => [ | n] /= Df. by []. apply is_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. eapply filterdiff_ext_lin. apply @filterdiff_comp'. apply @filterdiff_plus_fct ; try by apply locally_filter. by apply filterdiff_id. by apply filterdiff_const. by apply Df. simpl => y. by rewrite plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv