proposition: Lemma is_derive_n_opp (f : R -> R) (n : nat) (x l : R) : is_derive_n f n x l -> is_derive_n (fun x => -f x) n x (- l).
proof: Proof. case: n x => [ | n] /= x Hf. by rewrite Hf. apply is_derive_opp in Hf. apply: is_derive_ext Hf. move => y ; by rewrite Derive_n_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv