proposition: Lemma expf_card x : x ^+ #|F| = x :> F.
proof: Proof. rewrite -[RHS]mulr1 -(ltn_predK (finRing_gt1 F)) exprS. apply/eqP; rewrite -subr_eq0 -mulrBr mulf_eq0 subr_eq0 -implyNb -unitfE. apply/implyP=> Ux; rewrite -(val_unitX _ (Sub x _)) -val_unit1 val_eqE. by rewrite -order_dvdn -card_finField_unit order_dvdG ?inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)