proposition: Lemma morph_gacent A : A \subset D1 -> h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A).
proof: Proof. have [[_ defD2] [injh defR2]] := (isomP iso_f, isomP iso_h). move=> sAD1; rewrite !gacentE //; last by rewrite -defD2 morphimS. rewrite morphimEsub ?subsetIl // -{1}defR2 morphimEdom. exact: (morph_afix (gact_stable to1) (injmP injh)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)