proposition: Lemma complex_triangle_turn (a b c : C) (z : C) : complex_triangle a b c z -> complex_triangle b c a z.
proof: Proof. intros (a',(b',(c',(Ha,(Hb,(Hc,(Habs,->))))))). exists b', c', a'. replace (b' + c' + a')%R with (a' + b' + c')%R by ring. repeat split => //. rewrite Cplus_comm Cplus_assoc. by rewrite Cplus_comm Cplus_assoc. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)