proposition: Lemma complex_triangle_diameter_ball (a b c z0 : C) (eps : R) : (complex_triangle_diameter a b c < eps) -> (complex_triangle a b c z0) -> forall z, complex_triangle a b c z -> ball z0 eps z.
proof: Proof. intros Heps Hz0 z Hz. apply (norm_compat1 (V := C_NormedModule)). eapply Rle_lt_trans, Heps => {Heps}. by apply complex_triangle_diameter_le. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)