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