proposition: Lemma pquo_plength1 G H : H <| G -> p.-group H -> 'O_p^'(G / H) = 1-> p.-length_1 (G / H) = p.-length_1 G.
proof: Proof. rewrite /plength_1 => nHG pH trO; apply/idP/idP; last exact: plength1_quo. rewrite (pseries_pop _ trO) => pGH1; rewrite eqEsubset pseries_sub /=. rewrite pseries_pop //; last first. apply/eqP; rewrite -subG1; have <-: H :&: 'O_p^'(G) = 1. by apply: coprime_TIg; apply: pnat_coprime (pcore_pgroup _ _). rewrite setIC subsetI subxx -quotient_sub1. by rewrite -trO morphim_pcore. exact/gFsub_trans/normal_norm. have nOG: 'O_{p}(G) <| G by apply: pseries_normal. rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _]) //. have [|f f_inj im_f] := third_isom _ nHG nOG. by rewrite /= pseries1 pcore_max. rewrite (quotient_pseries [::_]) -{}im_f //= -injmF //. rewrite {f f_inj}morphimS // pseries1 -pquotient_pcore // -(pseries1 p) /=. by rewrite -quotient_pseries /= (eqP pGH1). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)