proposition: Lemma memv_preim f u W : (f u \in W) = (u \in f @^-1: W)%VS.
proof: Proof. apply/idP/idP=> [Wfu | /(memv_img f)]; last first. by rewrite -lpreim_cap_limg lpreimK ?capvSr // => /memv_capP[]. rewrite -[u](addNKr (f^-1%VF (f u))) memv_add ?memv_img //. by rewrite memv_cap Wfu memv_img ?memvf. by rewrite memv_ker addrC linearB /= subr_eq0 limg_lfunVK ?memv_img ?memvf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)