proposition: Lemma gFisog gT rT (G : {group gT}) (R : {group rT}) : G \isog R -> F gT G \isog F rT R.
proof: Proof. by case/isogP=> f injf <-; rewrite -injmF // sub_isog ?gFsub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)