proposition: Lemma poly_modnp_Xn n k v : 0 < k -> 1 < n -> PolyZ n k (modnp_Xn n k v) = rmodp 'X^v ('X^k - 1).
proof: Proof. move=> k_gt0 n_gt1. have XnM:= monic_Xn_sub_1 [ringType of 'Z_n] k_gt0. rewrite [in 'X^ _](divn_eq v k) exprD mulnC. rewrite -{1}['X^(_ * _)](subrK 1) mulrDl. rewrite rmodpD // mul1r -rmodp_mulml // rmodp_Xn_sub1 //. rewrite mul0r rmod0p add0r rmodp_small; last first. by rewrite size_polyXn size_Xn_sub_1 // ltnS ltn_mod. apply/polyP => i. rewrite /PolyZ coef_Poly coefXn. case: (leqP k i) => iLk. have k1Li1 : k.-1 <= i.-1 by rewrite -ltnS !prednK // (leq_trans k_gt0). rewrite nth_default; last by rewrite size_map size_take size_modnp_Xn // ltnn. by case: eqP => // iE; move: iLk; rewrite iE leqNgt ltn_mod k_gt0. rewrite (nth_map 0%N); last by rewrite size_take size_modnp_Xn // ltnn. rewrite nth_take // nth_cat size_nseq nth_nseq if_same. case: ltngtP => iLv; first by rewrite inZp0. rewrite -cat1s nth_cat /= ifF. by rewrite nth_nseq if_same inZp0. by rewrite ltnNge -(subnn (v %% k)%N) ltn_sub2r. by rewrite iLv subnn. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound