proposition: Lemma generator_coprime m : generator <[a]> (a ^+ m) = coprime #[a] m.
proof: Proof. rewrite /generator eq_sym eqEcard cycleX -/#[a] [#|_|]orderXgcd /=. apply/idP/idP=> [le_a_am|co_am]; last by rewrite (eqnP co_am) divn1. have am_gt0: 0 < gcdn #[a] m by rewrite gcdn_gt0 order_gt0. by rewrite /coprime eqn_leq am_gt0 andbT -(@leq_pmul2l #[a]) ?muln1 -?leq_divRL. 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)