proposition: Lemma complex_triangle_perimeter_turn (a b c : C) : complex_triangle_perimeter a b c = complex_triangle_perimeter b c a.
proof: Proof. unfold complex_triangle_perimeter ; ring. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)