proposition: Lemma rV_of_nat_neq0 i : i <> O -> (i < expn 2 n)%nat -> rV_of_nat n i <> 0%R.
proof: Proof. move=> Hi W. move: (bitseq_of_nat_nseq_false Hi W) => H. contradict H. apply eq_from_nth with false. - by rewrite /= size_pad_seqL size_nseq. - move=> j Hj. rewrite (_ : size _ = n) in Hj; last by apply/eqP; rewrite size_bitseq_of_nat. move/rowP : H => /(_ (Ordinal Hj)). rewrite !mxE /= => Hj'. rewrite nth_nseq Hj. by apply F2_of_bool_0_inv. 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