proposition: Lemma order_inj_cyclic : {in G &, forall x y, #[x] = #[y] -> <[x]> = <[y]>} -> cyclic G.
proof: Proof. move=> ucG; apply: negbNE (contra _ (negbT (ltnn #|G|))) => ncG. rewrite -{2}[#|G|]sum_totient_dvd big_mkcond (bigD1 ord_max) ?dvdnn //=. rewrite -{1}[#|G|]sum_ncycle_totient (bigD1 ord_max) //= -addSn leq_add //. rewrite eq_card0 ?totient_gt0 ?cardG_gt0 // => C. apply/imsetP=> [[x /setIdP[Gx /eqP oxG]]]; case/cyclicP: ncG. by exists x; apply/eqP; rewrite eq_sym eqEcard cycle_subG Gx -oxG /=. elim/big_ind2: _ => // [m1 n1 m2 n2 | d _]; first exact: leq_add. set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0. rewrite {}/Gd => /imsetP[x /setIdP[Gx /eqP <-] _ {C d}]. rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C. apply/idP/eqP=> [|-> {C}]; last by rewrite imset_f // inE Gx eqxx. by case/imsetP=> y /setIdP[Gy /eqP/ucG->]. 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)