proposition: Lemma prodv_line u v : (<[u]> * <[v]> = <[u * v]>)%VS.
proof: Proof. apply: subv_anti; rewrite -memvE memv_mul ?memv_line // andbT. apply/prodvP=> _ _ /vlineP[a ->] /vlineP[b ->]. by rewrite -scalerAr -scalerAl !memvZ ?memv_line. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)