proposition: Lemma ex_derive_n_comp_opp (f : R -> R) (n : nat) (x : R) : locally (- x) (fun y => (forall k, (k <= n)%nat -> ex_derive_n f k y)) -> ex_derive_n (fun y => f (- y)) n x.
proof: Proof. move => Hf. apply (ex_derive_n_ext (fun y : R => f (-1 * y))). move => t ; by ring_simplify (-1*t). apply (ex_derive_n_comp_scal f (-1) n x). by replace (-1*x) with (-x) by ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv