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