proposition: Lemma sub_der1_norm G H : G^`(1) \subset H -> H \subset G -> G \subset 'N(H).
proof: Proof. by move=> sG'H sHG; rewrite -commg_subr (subset_trans _ sG'H) ?commgS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)