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