proposition: Lemma dvdn_morphim G : #|f @* G| %| #|G|.
proof: Proof. rewrite card_morphim (dvdn_trans (dvdn_indexg _ _)) //. by rewrite cardSg ?subsetIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)