proposition: Lemma morphim_sol : solvable G -> solvable (f @* G).
proof: Proof. move/(solvableS (subsetIr D G)); case/derivedP=> n Gn1; apply/derivedP. by exists n; rewrite /= -morphimIdom -morphim_der ?subsetIl // 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)