proposition: Lemma Ohm1_cyclic_pgroup_prime p G : cyclic G -> p.-group G -> G :!=: 1 -> #|'Ohm_1(G)| = p.
proof: Proof. move=> cycG pG ntG; set K := 'Ohm_1(G). have abelK: p.-abelem K by rewrite Ohm1_abelem ?cyclic_abelian. have sKG: K \subset G := Ohm_sub 1 G. case/cyclicP: (cyclicS sKG cycG) => x /=; rewrite -/K => defK. rewrite defK -orderE (abelem_order_p abelK) //= -/K ?defK ?cycle_id //. rewrite -cycle_eq1 -defK -(setIidPr sKG). by apply: contraNneq ntG => /TI_Ohm1; rewrite setIid => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)