proposition: Lemma injm_sol : 'injm f -> G \subset D -> solvable (f @* G) = solvable G.
proof: Proof. move=> injf sGD; apply/idP/idP; last exact: morphim_sol. case/derivedP=> n Gn1; apply/derivedP; exists n; apply/trivgP. by rewrite -(injmSK injf) ?gFsub_trans ?morphim_der // Gn1 morphim1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)