proposition: Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p : G \isog H -> (G \homg Grp p) = (H \homg Grp p).
proof: Proof. by rewrite isogEhom => /andP[homGH homHG]; apply/idP/idP; apply: homGrp_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)