proposition: Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U <= V)%VS).
proof: Proof. apply: (iffP idP) => [|[u Uu]]; last by apply: contra => /subvP->. case/row_subPn=> i; set vi := row i _ => V'vi. by exists (r2v vi); rewrite memvK r2vK ?row_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)