proposition: Lemma prodv0 : right_zero 0%VS prodv.
proof: Proof. move=> U; apply/eqP; rewrite -dimv_eq0 -leqn0 (leq_trans (dim_prodv U 0)) //. by rewrite dimv0 muln0. 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)