proposition: Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p -> G \homg Grp p.
proof: Proof. by move <-; apply: homg_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)