proposition: Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) : G \isog Grp p -> reflect (#|H| = #|G| /\ H \homg Grp p) (H \isog G).
proof: Proof. move=> isoGp; apply: (iffP idP) => [isoGH | [oH homHp]]. by rewrite (card_isog isoGH) -isoGp isog_hom. by rewrite isogEcard isoGp homHp /= oH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)