proposition: Lemma C_RInt_segm_norm f z1 z2 m : ex_C_RInt_segm f z1 z2 -> (forall z, complex_segment z1 z2 z -> Cmod (f z) <= m) -> Cmod (C_RInt_segm f z1 z2) <= m * (Cmod (z1 - z2)).
proof: Proof. intros. apply is_C_RInt_segm_norm with f. by apply C_RInt_segm_correct. by []. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)