proposition: Lemma snd_tnth_prod_rV n (x : {: 'rV[A]_n * 'rV[B]_n}) i : x.2 ``_ i = ((prod_rV x) ``_ i).2.
proof: Proof. by rewrite mxE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2