proposition: Lemma homg_quotientS (A : {set gT}) : A \subset 'N(H) -> A \subset 'N(K) -> H \subset K -> A / K \homg A / H.
proof: Proof. rewrite -!(gen_subG A) /=; set L := <<A>> => nHL nKL sKH. have sub_ker: 'ker (restrm nHL (coset H)) \subset 'ker (restrm nKL (coset K)). by rewrite !ker_restrm !ker_coset setIS. have sAL: A \subset L := subset_gen A; rewrite -(setIidPr sAL). rewrite -[_ / H](morphim_restrm nHL) -[_ / K](morphim_restrm nKL) /=. by rewrite -(morphim_factm sub_ker (subxx L)) morphim_homg ?morphimS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)