proposition: Lemma repr_classesP xG : reflect (repr xG \in G /\ xG = repr xG ^: G) (xG \in classes G).
proof: Proof. apply: (iffP imsetP) => [[x Gx ->] | []]; last by exists (repr xG). by have [y Gy ->] := repr_class x; rewrite classGidl ?groupJ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)