proposition: Lemma orderXpfactor p k n x : #[x ^+ (p ^ k)] = n -> prime p -> p %| n -> #[x] = (p ^ k * n)%N.
proof: Proof. move=> oxp p_pr dv_p_n. suffices pk_x: p ^ k %| #[x] by rewrite -oxp orderXdiv // mulnC divnK. rewrite pfactor_dvdn // leqNgt; apply: contraL dv_p_n => lt_x_k. rewrite -oxp -p'natE // -(subnKC (ltnW lt_x_k)) expnD expgM. rewrite (pnat_dvd (orderXdvd _ _)) // -p_part // orderXdiv ?dvdn_part //. by rewrite -{1}[#[x]](partnC p) // mulKn // part_pnat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)