proposition: Lemma chief_series_exists H G : H <| G -> {s | (G.-chief).-series 1%G s & last 1%G s = H}.
proof: Proof. have [m] := ubnP #|H|; elim: m H => // m IHm U leUm nsUG. have [-> | ntU] := eqVneq U 1%G; first by exists [::]. have [V maxV]: {V : {group gT} | maxnormal V U G}. by apply: ex_maxgroup; exists 1%G; rewrite proper1G ntU norms1. have /andP[ltVU nVG] := maxgroupp maxV. have [||s ch_s defV] := IHm V; first exact: leq_trans (proper_card ltVU) _. by rewrite /normal (subset_trans (proper_sub ltVU) (normal_sub nsUG)). exists (rcons s U); last by rewrite last_rcons. by rewrite rcons_path defV /= ch_s /chief_factor; apply/and3P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)