proposition: Lemma convC t a b : a <| t |> b = b <| 1 - t |> a.
proof: Proof. by rewrite/conv opprB addrCA subrr addr0 addrC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise