proposition: Lemma memv_imgP f w U : reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
proof: Proof. apply: (iffP idP) => [|[u Uu ->]]; last exact: memv_img. rewrite 2!unlock memvE /subsetv !genmxE => /submxP[ku Drw]. exists (r2v (ku *m vs2mx U)); last by rewrite /= r2vK -mulmxA -Drw v2rK. by rewrite memvE /subsetv !genmxE r2vK submxMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)