proposition: Lemma prod1v : left_id 1%VS prodv.
proof: Proof. move=> U; apply/subv_anti/andP; split. by apply/prodvP=> _ u /vlineP[a ->] Uu; rewrite mulr_algl memvZ. by apply/subvP=> u Uu; rewrite -[u]mul1r memv_mul ?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)