proposition: Lemma poly_modnp_mulX n k v : 0 < k -> 1 < n -> size v = k -> PolyZ n k (modnp_mulX n k v) = rmodp ('X * PolyZ n k v) ('X^k - 1).
proof: Proof. move=> k_gt0 n_gt1 vsE; rewrite !PolyZE. have xnM := monic_Xn_sub_1 [ringType of 'Z_n] k_gt0. rewrite mulr_sumr rmodp_sum //= -[k]prednK // big_ord_recl big_ord_recr addrC. congr (_ + _); last first. rewrite expr0 alg_polyC -scalerAr -exprS rmodpZ ?prednK //. rewrite [in 'X^_]prednK // [in modnp_mulX _ _]prednK //. rewrite -{1}['X^k](subrK 1) // rmodpD // rmodpp // add0r. rewrite rmodp_small; last by rewrite size_poly1 size_Xn_sub_1. rewrite alg_polyC; congr (_%:P). apply/val_eqP; rewrite /= Zp_cast // /modnp_mulX. case: v vsE => [|a v1 <- /=]; first by rewrite nth_nil. by rewrite (last_nth 0%N). apply: eq_bigr => j _. rewrite -scalerAr -exprS rmodpZ ?prednK //. congr (inZp _ *: _); last first. rewrite rmodp_small //= prednK // size_Xn_sub_1 //. by rewrite size_polyXn !ltnS -{2}[k]prednK // ltnS ltn_ord. rewrite /modnp_mulX [in RHS]/= nth_belast_max //=. by rewrite vsE -[X in _ < X]prednK // ltnS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound