proposition: Lemma expr_dvd n x i : x ^+ n = 1 -> n %| i -> x ^+ i = 1.
proof: Proof. by move=> xn1 dvd_n_i; rewrite -(expr_mod i xn1) (eqnP dvd_n_i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)