proposition: Lemma expr_mod n x i : x ^+ n = 1 -> x ^+ (i %% n) = x ^+ i.
proof: Proof. move=> xn1; rewrite {2}(divn_eq i n) exprD mulnC exprM xn1. by rewrite expr1n mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)