proposition: Lemma complex_triangle_diameter_swap (a b c : C) : complex_triangle_diameter a b c = complex_triangle_diameter a c b.
proof: Proof. unfold complex_triangle_diameter. rewrite -3!(Cmod_opp (_-_)) !Copp_minus_distr. rewrite Rmax_comm -Rmax_assoc. apply f_equal, Rmax_comm. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)