proposition: Lemma nat_of_rV_eq0 (y : 'rV_n) : (nat_of_rV y == O) = (y == 0).
proof: Proof. case/boolP : (nat_of_rV _ == O) => H. have : rV_of_nat n (nat_of_rV y) = 0 by rewrite (eqP H) rV_of_nat_0. by rewrite nat_of_rVK => ->; rewrite eqxx. apply/esym/eqP/eqP; apply: contra H => /eqP ->. by rewrite 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