proposition: Lemma solvable_norm_abelem L G : solvable G -> G <| L -> G :!=: 1 -> exists H : {group gT}, [/\ H \subset G, H <| L, H :!=: 1 & is_abelem H].
proof: Proof. move=> solG /andP[sGL nGL] ntG. have [H minH sHG]: {H : {group gT} | minnormal H L & H \subset G}. by apply: mingroup_exists; rewrite ntG. have [nHL ntH abH] := minnormal_solvable minH sHG solG. by exists H; split; rewrite // /normal (subset_trans sHG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)