proposition: Lemma complex_triangle_perimeter_swap (a b c : C) : complex_triangle_perimeter a b c = complex_triangle_perimeter a c b.
proof: Proof. unfold complex_triangle_perimeter. rewrite -3!(Cmod_opp (_-_)) !Copp_minus_distr ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)