proposition: Lemma quotient_cents2r A B K : [~: A, B] \subset K -> (A / K) \subset 'C(B / K).
proof: Proof. move=> sABK; rewrite -2![_ / _]morphimIdom -!quotientE. by rewrite quotient_cents2 ?subsetIl ?(subset_trans _ sABK) ?commgSS ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)