proposition: Lemma expg_zneg G x (k : 'Z_(#|G|)) : x \in G -> x ^+ (- k)%R = x ^- k.
proof: Proof. move=> Gx; apply/eqP; rewrite eq_sym eq_invg_mul -expgD. by rewrite -(expg_znat _ Gx) natrD natr_Zp natr_negZp subrr. 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)