proposition: Lemma abelem_order_p p G x : p.-abelem G -> x \in G -> x != 1 -> #[x] = p.
proof: Proof. case/and3P=> pG _ eG Gx; rewrite -cycle_eq1 => ntX. have{ntX} [p_pr p_x _] := pgroup_pdiv (mem_p_elt pG Gx) ntX. by apply/eqP; rewrite eqn_dvd p_x andbT order_dvdn (exponentP eG). 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)