proposition: Lemma Derive_n_opp (f : R -> R) (n : nat) (x : R) : Derive_n (fun x => - f x) n x = - Derive_n f n x.
proof: Proof. elim: n x => [ | n IH] x /=. by []. rewrite -Derive_opp. by apply Derive_ext. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv