proposition: Lemma locally_C_segm (P : C -> Prop) : forall z0, locally z0 P -> locally z0 (fun z => forall y, complex_segment z0 z y -> P y).
proof: Proof. intros z0 (e,He). assert (Hd : 0 < e / (norm_factor (V := C_NormedModule))). apply Rdiv_lt_0_compat. by apply e. by apply norm_factor_gt_0. set (d := mkposreal _ Hd). exists d => z Hz _ [x [Hx ->]]. apply He. apply (norm_compat1 (V := C_NormedModule)). change minus with Cminus ; change norm with Cmod. replace (scal (1 - x)%R z0 + scal x z - z0) with (x * (z - z0)). 2: rewrite !scal_R_Cmult RtoC_minus /= ; by ring_simplify. rewrite Cmod_mult. eapply Rle_lt_trans. apply Rmult_le_compat_r. by apply Cmod_ge_0. rewrite Cmod_R Rabs_pos_eq ; apply Hx. rewrite Rmult_1_l. replace (pos e) with ((norm_factor (V := C_NormedModule)) * d)%R. by apply (norm_compat2 (V := C_NormedModule)). rewrite /d /= ; field. by apply Rgt_not_eq, norm_factor_gt_0. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)