proposition: Lemma mem_repr_coset xbar : repr xbar \in xbar.
proof: Proof. by case: xbar => /= _ /rcosetsP[x _ ->]; apply: mem_repr_rcoset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)