proposition: Lemma convlr t a b : a <| t |> b = a + (1 - t) *: (b-a).
proof: Proof. by rewrite scalerDr scalerN addrCA -{2}[a]scale1r -scalerBl opprB addrCA subrr addr0 addrC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise