proposition: Lemma comm_norm_cent_cent H G K : H \subset 'N(G) -> H \subset 'C(K) -> G \subset 'N(K) -> [~: G, H] \subset 'C(K).
proof: Proof. move=> nGH /centsP cKH nKG; rewrite commGC gen_subG centsC. apply/centsP=> x Kx _ /imset2P[y z Hy Gz ->]; red. rewrite mulgA -[x * _]cKH ?groupV // -!mulgA; congr (_ * _). rewrite (mulgA x) (conjgC x) (conjgCV z) 3!mulgA; congr (_ * _). by rewrite -2!mulgA (cKH y) // -mem_conjg (normsP nKG). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)