proposition: Lemma mem_p_elt pi x G : pi.-group G -> x \in G -> pi.-elt x.
proof: Proof. by move=> piG Gx; apply: pgroupS piG; rewrite cycle_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)