proposition: Lemma continuous_C_segm (f : C -> C) (z1 z2 : C) : (forall z : C, complex_segment z1 z2 z -> continuous f z) -> (forall z : R, 0 <= z <= 1 -> continuous (fun t : R => (z2 - z1) * f (scal (1 - t)%R z1 + scal t z2)) z).
proof: Proof. intros Cf z Hz. apply @continuous_scal. apply continuous_const. apply continuous_comp. apply @continuous_plus. apply (continuous_scal_l (K := R_AbsRing) (V := C_R_NormedModule)). apply @continuous_minus. apply continuous_const. apply continuous_id. apply (continuous_scal_l (K := R_AbsRing) (V := C_R_NormedModule)). apply continuous_id. apply Cf. by exists z. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)