proposition: Lemma max_unity_roots rs : n > 0 -> all n.-unity_root rs -> uniq rs -> size rs <= n.
proof: Proof. move=> n_gt0 rs_n_1 Urs; have szPn := size_Xn_sub_1 F n_gt0. by rewrite -ltnS -szPn max_poly_roots -?size_poly_eq0 ?szPn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)