proposition: Lemma second_isom : {f : {morphism H / (K :&: H) >-> coset_of K} | 'injm f & forall A : {set gT}, A \subset H -> f @* (A / (K :&: H)) = A / K}.
proof: Proof. have ->: K :&: H = 'ker_H (coset K) by rewrite ker_coset setIC. exact: first_isom_loc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)