proposition: Lemma prim_rootP x : x ^+ n = 1 -> {i : 'I_n | x = z ^+ i}.
proof: Proof. move=> xn1; pose logx := [pred i : 'I_n | x == z ^+ i]. case: (pickP logx) => [i /eqP-> | no_i]; first by exists i. case: notF; suffices{no_i}: x \in zn. case/mapP=> i; rewrite mem_index_iota => lt_i_n def_x. by rewrite -(no_i (Ordinal lt_i_n)) /= -def_x. rewrite -root_prod_XsubC big_map factor_Xn_sub_1. by rewrite [root _ x]unity_rootE xn1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)