proposition: Lemma coset_id x : x \in A -> coset x = 1.
proof: Proof. by move=> Ax; apply: coset_mem; apply: mem_gen. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)