proposition: Lemma is_C_RInt_segm_derive (f g : C -> C) (z1 z2 : C) : (forall z, complex_segment z1 z2 z -> is_derive g z (f z)) -> (forall z, complex_segment z1 z2 z -> continuous f z) -> is_C_RInt_segm f z1 z2 (g z2 - g z1).
proof: Proof. intros Dg Cf. unfold is_C_RInt_segm. evar_last. apply (is_C_RInt_derive (fun t : R => g (scal (1 - t)%R z1 + scal t z2)) (fun t => (z2 - z1) * f (scal (1 - t)%R z1 + scal t z2))). rewrite /Rmin /Rmax ; case: Rle_dec Rle_0_1 => // _ _. intros. eapply filterdiff_ext_lin. apply (filterdiff_comp' (U := R_NormedModule) (V := C_R_NormedModule) (fun t : R => (scal (1 - t)%R z1 + scal t z2)%C) g). apply @filterdiff_plus_fct. apply locally_filter. apply (filterdiff_scal_l_fct (U := R_NormedModule) (V := C_R_NormedModule) z1 (fun u : R => (1 - u)%R)). apply @filterdiff_minus_fct. by apply locally_filter. apply filterdiff_const. apply filterdiff_id. apply filterdiff_linear. move: (is_linear_scal_l (V := C_R_NormedModule) z2) => //=. apply is_derive_filterdiff_C_R. instantiate (1 := (fun y => y * f (scal (1 - x)%R z1 + scal x z2))). apply (is_linear_comp (U := C_NormedModule) (V := AbsRing_NormedModule C_AbsRing) (fun y => y)). apply is_linear_C_id_1. apply @is_linear_scal_l. simpl ; rewrite Cmult_1_l. apply Dg. by exists x. simpl. rewrite /= /scal /= /mult /= /prod_scal. change scal with Rmult. change plus with Cplus. change minus with Rminus. change zero with 0. intros y ; apply injective_projections ; simpl ; ring. rewrite /Rmin /Rmax ; case: Rle_dec Rle_0_1 => // _ _. by apply continuous_C_segm. rewrite Rminus_eq_0 Rminus_0_r !scal_one !scal_zero_l. by rewrite Cplus_0_l Cplus_0_r. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)