proposition: Lemma rV_of_nat_inj i j : (i < expn 2 n)%nat -> (j < expn 2 n)%nat -> rV_of_nat n i = rV_of_nat n j -> i = j.
proof: Proof. move=> Hi Hj /bitseq_row_nth => h; apply (@bitseq_of_nat_inj n) => //. by apply h; rewrite !(eqP (size_bitseq_of_nat _ _)). 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