proposition: Lemma gacentM G H : G \subset D -> H \subset D -> 'C_(|to)(G * H) = 'C_(|to)(G) :&: 'C_(|to)(H).
proof: Proof. by move=> sGD sHB; rewrite -gacent_gen ?mul_subG // genM_join gacentY. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)