proposition: Lemma intro_isoGrp gT (G : {group gT}) p : G \homg Grp p -> (forall rT (H : {group rT}), H \homg Grp p -> H \homg G) -> G \isog Grp p.
proof: Proof. move=> homGp freeG rT H. by apply/idP/idP=> [homHp|]; [apply: homGrp_trans homGp | apply: freeG]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)