proposition: Lemma expg_znat G x k : x \in G -> x ^+ (k%:R : 'Z_(#|G|))%R = x ^+ k.
proof: Proof. case: (eqsVneq G 1) => [-> /set1P-> | ntG Gx]; first by rewrite !expg1n. apply/eqP; rewrite val_Zp_nat ?cardG_gt1 // eq_expg_mod_order. by rewrite modn_dvdm ?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)