proposition: Lemma cosetpre_set1 x : x \in 'N(H) -> coset H @*^-1 [set coset H x] = H :* x.
proof: Proof. by rewrite -{9}ker_coset; apply: morphpre_set1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)