proposition: Lemma rV_of_nat_0 : rV_of_nat n 0 = 0.
proof: Proof. rewrite /rV_of_nat /row_of_bitseq; apply/rowP => b /=. by rewrite !mxE bitseq_of_nat_0 nth_nseq (ltn_ord b). 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