proposition: Lemma subvP U V : reflect {subset U <= V} (U <= V)%VS.
proof: Proof. apply: (iffP rV_subP) => sU12 u. by rewrite !memvE /subsetv !genmxE => /sU12. by have:= sU12 (r2v u); rewrite !memvE /subsetv !genmxE r2vK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)