proposition: Lemma quotient_normG G : H <| G -> 'N(G) / H = 'N(G / H).
proof: Proof. case/andP=> sHG nHG. by rewrite [_ / _]morphim_normG ?ker_coset // im_coset setTI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)