proposition: Lemma card_homg (aT rT : finGroupType) (G : {group aT}) (R : {group rT}) : G \homg R -> #|G| %| #|R|.
proof: Proof. by case/homgP=> f <-; rewrite card_morphim setIid dvdn_indexg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)