proposition: Lemma factor_Xn_sub_1 : \prod_(0 <= i < n) ('X - (z ^+ i)%:P) = 'X^n - 1.
proof: Proof. transitivity (\prod_(w <- zn) ('X - w%:P)); first by rewrite big_map. have n_gt0: n > 0 := prim_order_gt0 prim_z. rewrite (@all_roots_prod_XsubC _ ('X^n - 1) zn); first 1 last. - by rewrite size_Xn_sub_1 // size_map size_iota subn0. - apply/allP=> _ /mapP[i _ ->] /=; rewrite rootE !hornerE. by rewrite exprAC (prim_expr_order prim_z) expr1n subrr. - rewrite uniq_rootsE map_inj_in_uniq ?iota_uniq // => i j. rewrite !mem_index_iota => ltin ltjn /eqP. by rewrite (eq_prim_root_expr prim_z) !modn_small // => /eqP. by rewrite (monicP (monic_Xn_sub_1 F n_gt0)) scale1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)