proposition: Lemma inv_quotientN : Kbar <| G / H -> inv_quotient_spec (fun K => K <| G).
proof: Proof. move=> nKbar; case/inv_quotientS: (normal_sub nKbar) => K defKbar sHK sKG. exists K => //; rewrite defKbar -cosetpre_normal !quotientGK // in nKbar. exact: normalS nHG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)