proposition: Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.
proof: Proof. rewrite -{2}(addv_diff_cap U (lker f)) limgD; apply/esym/addv_idPl. by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)