proposition: Lemma ex_C_RInt_segm_continuous f z1 z2 : (forall z, complex_segment z1 z2 z -> continuous f z) -> ex_C_RInt_segm f z1 z2.
proof: Proof. intros Cf. apply (ex_RInt_continuous (V := C_R_CompleteNormedModule)). rewrite /Rmin /Rmax ; case: Rle_dec Rle_0_1 => // _ _. by apply continuous_C_segm. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)