proposition: Lemma eq_expg_ord (gT : finGroupType) (x : gT) d (n m : 'I_d) : (d <= #[x]%g)%N -> ((x ^+ m)%g == (x ^+ n)%g) = (m == n).
proof: Proof. by move=> d_leq; rewrite eq_expg_mod_order !modn_small// (leq_trans _ d_leq). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)