proposition: Lemma gacent_comp U : 'C_(|comp_groupAction)(U) = 'C_(|to)(f @* U).
proof: Proof. rewrite /gacent afix_comp ?subIset ?subxx //. by rewrite -(setIC U) (setIC D) morphim_setIpre. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)