proposition: Lemma is_C_RInt_segm_norm (f : C -> C) (z1 z2 : C) lf (m : R) : is_C_RInt_segm f z1 z2 lf -> (forall z, complex_segment z1 z2 z -> Cmod (f z) <= m) -> Cmod lf <= m * (Cmod (z1 - z2)).
proof: Proof. intros Cf Hm. rewrite 2!Cmod_norm. apply: (norm_RInt_le (fun t => (z2 - z1) * f (scal (1 - t)%R z1 + scal t z2)) (fun _ => Rmult (Cmod (z2 - z1)) m) 0 1). by apply Rle_0_1. intros x Hx. rewrite <- Cmod_norm. rewrite Cmod_mult. apply Rmult_le_compat_l. by apply Cmod_ge_0. apply Hm. now exists x ; split. by apply Cf. evar_last. apply is_RInt_const. rewrite -Cmod_norm -Cmod_opp Copp_minus_distr ; simpl. rewrite /scal /= /mult /=. ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)