proposition: Lemma nat_of_rVK (y : 'rV_n) : rV_of_nat n (nat_of_rV y) = y.
proof: Proof. case: n y => [|n0] y. apply/rowP; by case. apply/rowP => i. rewrite mxE /nat_of_rV. set tmp := [seq bool_of_F2 i | i <- _]. rewrite [X in bitseq_of_nat _ X](_ : _ = size tmp); last by rewrite size_map size_tuple. rewrite N_of_bitseqK; last by rewrite size_tuple. rewrite /tmp (nth_map (0 : 'F_2)); last by rewrite size_tuple. by rewrite bool_of_F2K /tuple_of_row nth_mktuple. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext mathcomp(bigop zmodp ssralg matrix) ssralg_ext f2