proposition: Lemma eq_expg_mod_order m n : (a ^+ m == a ^+ n) = (m == n %[mod #[a]]).
proof: Proof. have [->|] := eqVneq a 1; first by rewrite order1 !modn1 !expg1n eqxx. rewrite -order_gt1 => lt1a; have ZpT: Zp #[a] = setT by rewrite /Zp lt1a. have: injective Zpm by move=> i j; apply (injmP injm_Zpm); rewrite /= ZpT inE. move/inj_eq=> eqZ; symmetry; rewrite -(Zp_cast lt1a). by rewrite -[_ == _](eqZ (inZp m) (inZp n)) /Zpm /= Zp_cast ?expg_mod_order. 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)