proposition: Lemma chief_factor_minnormal G V U : chief_factor G V U -> minnormal (U / V) (G / V).
proof: Proof. case/andP=> maxV /andP[sUG nUG]; apply: maxnormal_minnormal => //. by have /andP[_ nVG] := maxgroupp maxV; apply: subset_trans sUG nVG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)