proposition: Lemma ex_derive_opp : forall (f : K -> V) (x : K), ex_derive f x -> ex_derive (fun x => opp (f x)) x.
proof: Proof. intros f x [df Df]. eexists. apply is_derive_opp. exact Df. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv