proposition: Lemma mem_repr_classes xG : xG \in classes G -> repr xG \in xG.
proof: Proof. by case/repr_classesP=> _ {2}->; apply: class_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)