proposition: Lemma C_derive_correct (f : C -> C) (z l : C) : ex_derive f z -> is_derive f z (C_derive f z).
proof: Proof. case => df Hf. replace (C_derive f z) with df => //. by apply sym_eq, is_C_derive_unique. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy