proposition: Lemma limg_ker0 f U V : lker f == 0%VS -> (f @: U <= f @: V)%VS = (U <= V)%VS.
proof: Proof. move/lker0P=> injf; apply/idP/idP=> [/subvP sfUV | ]; last exact: limgS. by apply/subvP=> u Uu; have /memv_imgP[v Vv /injf->] := sfUV _ (memv_img f Uu). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)