proposition: Lemma quotient_subcent1 A x : 'C_A[x] / H \subset 'C_(A / H)[coset H x].
proof: Proof. exact: subset_trans (quotientI _ _) (setIS _ (quotient_cent1 x)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)