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