proposition: Lemma complex_triangle_diameter_turn (a b c : C) : complex_triangle_diameter a b c = complex_triangle_diameter b c a.
proof: Proof. unfold complex_triangle_diameter. apply sym_eq ; rewrite Rmax_assoc. apply Rmax_comm. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)