proposition: Lemma injm_cyclem : 'injm (cyclem (val u) a).
proof: Proof. apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. have [a1 | nta] := eqVneq a 1; first by rewrite a1 cycle1 inE in ax. rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. by rewrite dvdn_gcd [in X in X && _]Zp_cast ?order_gt1 // order_dvdG. 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)