proposition: Lemma morph_gastabs S : S \subset R1 -> f @* 'N(S | to1) = 'N(h @* S | to2).
proof: Proof. have [[_ defD2] [injh _]] := (isomP iso_f, isomP iso_h). move=> sSR1; rewrite (morphimEsub _ sSR1). apply: (morph_astabs (gact_stable to1) (injmP injh)) => // u x. by move/(subsetP sSR1); apply: hfJ. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)