proposition: Lemma inv_quotientS : Kbar \subset G / H -> inv_quotient_spec (fun K => K \subset G).
proof: Proof. case/andP: nHG => sHG nHG' sKbarG. have sKdH: Kbar \subset 'N(H) / H by rewrite (subset_trans sKbarG) ?morphimS. exists (coset H @*^-1 Kbar)%G; first by rewrite cosetpreK. by rewrite -{1}ker_coset morphpreS ?sub1G. by rewrite sub_cosetpre_quo. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)