proposition: Lemma class_disj x y : y \notin x ^: G -> x ^: G :&: y ^: G = set0.
proof: Proof. Proof using. move/class_eqP=> xy. apply /setP=> a; rewrite !inE. apply /andP => [][/class_eqP ax /class_eqP ay]. by apply xy; rewrite -ax -ay. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent