proposition: Lemma piOhm1 G : \pi('Ohm_1(G)) = \pi(G).
proof: Proof. apply/eq_piP => p; apply/idP/idP; first exact: (piSg (Ohm_sub 1 G)). rewrite !mem_primes !cardG_gt0 => /andP[p_pr /Cauchy[] // x Gx oxp]. by rewrite p_pr -oxp order_dvdG //= Ohm1Eprime mem_gen // inE Gx oxp. 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)