fact: Definition nat_of_rV (y : 'rV['F_2]_n) : nat := BinNat.N.to_nat (N_of_bitseq (map bool_of_F2 (tuple_of_row y))).
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