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