proposition: Lemma rV_prodK n (x : 'rV[A * B]_n) : prod_rV (rV_prod x) = x.
proof: Proof. apply/rowP => b; rewrite !mxE; by case: (x ``_ b). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2