proposition: Lemma exponent_Ohm1_class2 H : odd p -> p.-group H -> nil_class H <= 2 -> exponent 'Ohm_1(H) %| p.
proof: Proof. move=> odd_p pH; rewrite nil_class2 => sH'Z; apply/exponentP=> x /=. rewrite (OhmE 1 pH) expn1 gen_set_id => {x} [/LdivP[] //|]. apply/group_setP; split=> [|x y]; first by rewrite !inE group1 expg1n //=. case/LdivP=> Hx xp1 /LdivP[Hy yp1]; rewrite !inE groupM //=. have [_ czH]: [~ y, x] \in H /\ centralises [~ y, x] H. by apply/centerP; rewrite (subsetP sH'Z) ?mem_commg. rewrite expMg_Rmul ?xp1 ?yp1 /commute ?czH //= !mul1g. by rewrite bin2odd // -commXXg ?yp1 /commute ?czH // comm1g. 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)