proposition: Lemma cosetpre_gen C : 1 \in C -> coset H @*^-1 <<C>> = <<coset H @*^-1 C>>.
proof: Proof. by move=> C1; rewrite morphpre_gen ?sub_im_coset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)