proposition: Lemma inv_map_homC (f : 'End(L')) : (f @: limg iota <= limg iota)%VS -> (iota \o inv_map_hom f = f \o iota)%VF.
proof: Proof. move=> fiota; apply/lfunP => x. rewrite !comp_lfunE limg_lfunVK//. by rewrite memvE (subv_trans _ fiota)// -memvE !memv_img ?memvf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)