proposition: Lemma Cauchy p G : prime p -> p %| #|G| -> {x | x \in G & #[x] = p}.
proof: Proof. move=> p_pr; have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn pG. pose xpG := [pred x in G | #[x] == p]. have [x /andP[Gx /eqP] | no_x] := pickP xpG; first by exists x. have{pG n leGn IHn} pZ: p %| #|'C_G(G)|. suffices /dvdn_addl <-: p %| #|G :\: 'C(G)| by rewrite cardsID. have /acts_sum_card_orbit <-: [acts G, on G :\: 'C(G) | 'J]. by apply/actsP=> x Gx y; rewrite !inE -!mem_conjgV -centJ conjGid ?groupV. elim/big_rec: _ => // _ _ /imsetP[x /setDP[Gx nCx] ->] /dvdn_addl->. have ltCx: 'C_G[x] \proper G by rewrite properE subsetIl subsetIidl sub_cent1. have /negP: ~ p %| #|'C_G[x]|. case/(IHn _ (leq_trans (proper_card ltCx) leGn))=> y /setIP[Gy _] /eqP-oy. by have /andP[] := no_x y. by apply/implyP; rewrite -index_cent1 indexgI implyNb -Euclid_dvdM ?LagrangeI. have [Q maxQ _]: {Q | [max Q | p^'.-subgroup('C_G(G)) Q] & 1%G \subset Q}. by apply: maxgroup_exists; apply: psubgroup1. case/andP: (maxgroupp maxQ) => sQC; rewrite /pgroup p'natE // => /negP[]. apply: dvdn_trans pZ (cardSg _); apply/subsetP=> x /setIP[Gx Cx]. rewrite -sub1set -gen_subG (normal_sub_max_pgroup maxQ) //; last first. rewrite /normal subsetI !cycle_subG ?Gx ?cents_norm ?subIset ?andbT //=. by rewrite centsC cycle_subG Cx. rewrite /pgroup p'natE //= -[#|_|]/#[x]; apply/dvdnP=> [[m oxm]]. have m_gt0: 0 < m by apply: dvdn_gt0 (order_gt0 x) _; rewrite oxm dvdn_mulr. case/idP: (no_x (x ^+ m)); rewrite /= groupX //= orderXgcd //= oxm. by rewrite gcdnC gcdnMr mulKn. 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)