proposition: Lemma nat_of_rV_up (y : 'rV_n) : nat_of_rV y < expn 2 n.
proof: Proof. by rewrite /nat_of_rV N_of_bitseq_up // size_map size_tuple. 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