proposition: Lemma mem_unity_roots rs : n > 0 -> all n.-unity_root rs -> uniq rs -> size rs = n -> n.-unity_root =i rs.
proof: Proof. move=> n_gt0 rs_n_1 Urs sz_rs_n x; rewrite -topredE /=. apply/idP/idP=> xn1; last exact: (allP rs_n_1). apply: contraFT (ltnn n) => not_rs_x. by rewrite -{1}sz_rs_n (@max_unity_roots (x :: rs)) //= ?xn1 ?not_rs_x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)