proposition: Lemma conv1 a b : a <| 1 |> b = a.
proof: Proof. by rewrite/conv scale1r subrr scale0r addr0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise