proposition: Lemma prim_order_dvd i : (n %| i) = (z ^+ i == 1).
proof: Proof. move: n_gt0; rewrite -prim_expr_mod /dvdn -(ltn_mod i). case: {i}(i %% n)%N => [|i] lt_i; first by rewrite !eqxx. case/andP: prim_z => _ /forallP/(_ (Ordinal (ltnW lt_i)))/eqP. by rewrite unity_rootE eqn_leq andbC leqNgt lt_i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)