proposition: Lemma astabU : 'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to).
proof: Proof. by apply/setP=> a; rewrite !inE subUset; case: (a \in D). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)