proposition: Lemma cosetpre_cent1s C x : coset H @*^-1 C \subset 'C[x] -> C \subset 'C[coset H x].
proof: Proof. move=> sC; rewrite -cosetpreSK; apply: subset_trans (cosetpre_cent1 x). by rewrite subsetI subsetIl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)