proposition: Lemma orderXgcd a n : #[a ^+ n] = #[a] %/ gcdn #[a] n.
proof: Proof. apply/eqP; rewrite eqn_dvd; apply/andP; split. rewrite order_dvdn -expgM -muln_divCA_gcd //. by rewrite expgM expg_order expg1n. have [-> | n_gt0] := posnP n; first by rewrite gcdn0 divnn order_gt0 dvd1n. rewrite -(dvdn_pmul2r n_gt0) divn_mulAC ?dvdn_gcdl // dvdn_lcm. by rewrite order_dvdn mulnC expgM expg_order eqxx 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)