proposition: Lemma nat_of_rV_0 : nat_of_rV (0 : 'rV_n) = O.
proof: Proof. rewrite /nat_of_rV (_ : N_of_bitseq _ = 0%N) //. rewrite (_ : map _ _ = nseq n false) // ?N_of_bitseq_nseq_false //. apply eq_from_nth with false; first by rewrite size_map size_nseq size_tuple. move=> i; rewrite size_map size_tuple => ni. rewrite (nth_map 0) ?size_tuple // nth_nseq ni (_ : nth _ _ _ = 0) //. by rewrite /tuple_of_row /= (nth_map (Ordinal ni)) ?size_enum_ord // mxE. 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