proposition: Lemma card_morphim G : #|f @* G| = #|D :&: G : 'ker f|.
proof: Proof. rewrite -morphimIdom -indexgI -card_quotient; last first. by rewrite normsI ?normG ?subIset ?ker_norm. by apply: esym (card_isog _); rewrite first_isog_loc ?subsetIl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)