proposition: Lemma orderXexp p m n x : #[x] = (p ^ n)%N -> #[x ^+ (p ^ m)] = (p ^ (n - m))%N.
proof: Proof. move=> ox; have [n_le_m | m_lt_n] := leqP n m. rewrite -(subnKC n_le_m) subnDA subnn expnD expgM -ox. by rewrite expg_order expg1n order1. rewrite orderXdiv ox ?dvdn_exp2l ?expnB ?(ltnW m_lt_n) //. by have:= order_gt0 x; rewrite ox expn_gt0 orbC -(ltn_predK m_lt_n). 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)