proposition: Lemma orderXpnat m n x : #[x ^+ m] = n -> \pi(n).-nat m -> #[x] = (m * n)%N.
proof: Proof. move=> oxm n_m; have [m_gt0 _] := andP n_m. suffices m_x: m %| #[x] by rewrite -oxm orderXdiv // mulnC divnK. apply/dvdn_partP=> // p; rewrite mem_primes => /and3P[p_pr _ p_m]. have n_p: p \in \pi(n) by apply: (pnatP _ _ n_m). have p_oxm: p %| #[x ^+ (p ^ logn p m)]. apply: dvdn_trans (orderXdvd _ m`_p^'); rewrite -expgM -p_part ?partnC //. by rewrite oxm; rewrite mem_primes in n_p; case/and3P: n_p. by rewrite (orderXpfactor (erefl _) p_pr p_oxm) p_part // dvdn_mulr. 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)