proposition: Lemma quotient_isom : isom G (G / H) (restrm nHG (coset H)).
proof: Proof. by apply/isomP; rewrite ker_restrm setIC ker_coset tiHG im_restrm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)