proposition: Lemma memv_cosetP {U v w} : reflect (exists2 u, u\in U & w = u * v) (w \in U * <[v]>)%VS.
proof: Proof. rewrite -limg_amulr. by apply: (iffP memv_imgP) => [] [u] Uu ->; exists u; rewrite ?lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)