proposition: Lemma repr_class x : {y | y \in G & repr (x ^: G) = x ^ y}.
proof: Proof. set z := repr _; have: #|[set y in G | z == x ^ y]| > 0. have: z \in x ^: G by apply: (mem_repr x). by case/imsetP=> y Gy ->; rewrite (cardD1 y) inE Gy eqxx. by move/card_mem_repr; move: (repr _) => y /setIdP[Gy /eqP]; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)