proposition: Lemma prim_expr_order : z ^+ n = 1.
proof: Proof. case/andP: prim_z => _; rewrite -(prednK n_gt0) => /forallP/(_ ord_max). by rewrite unity_rootE eqxx eqb_id => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)