proposition: Lemma C_RInt_segm_derive (f : C -> C) (z1 z2 : C) : (forall z, complex_segment z1 z2 z -> ex_derive f z) -> (forall z, complex_segment z1 z2 z -> continuous (C_derive f) z) -> C_RInt_segm (C_derive f) z1 z2 = f z2 - f z1.
proof: Proof. intros. apply is_C_RInt_segm_unique, is_C_RInt_segm_derive => //. intros z Hz. by apply C_derive_correct, H. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)