proposition: Lemma der1_min G H : G \subset 'N(H) -> abelian (G / H) -> G^`(1) \subset H.
proof: Proof. by move=> nHG abGH; rewrite -quotient_cents2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)