proposition: Lemma nat_of_cV_0 k : nat_of_cV (0 : 'cV_k) = O.
proof: Proof. by rewrite /nat_of_cV trmx0 nat_of_rV_0. 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