proposition: Lemma poly_modnp_pow n k p v : 0 < k -> 1 < n -> size v = k -> PolyZ n k (modnp_pow n k p v) = rmodp (PolyZ n k v ^+ Pos.to_nat p) ('X^k - 1).
proof: Proof. move=> k_gt0 n_gt1 sv2E. have xnM := monic_Xn_sub_1 (GRing.Ring.clone _ 'Z_n) k_gt0. elim: p => [p1 IH|p1 IH|] /=; last first. - by rewrite expr1 rmodp_small // size_Xn_sub_1 // ltnS size_PolyZ. - rewrite poly_modnp_mul ?size_modnp_pow //= IH. rewrite rmodp_mulmr // rmodp_mulml // -exprD. by rewrite Pnat.Pos2Nat.inj_xO addnn -muln2 mulnC. rewrite !poly_modnp_mul ?(size_modnp_pow, size_modnp_mul) //= IH. rewrite rmodp_mulmr // mulrA rmodp_mulmr // mulrAC rmodp_mulmr //. by rewrite Pnat.Pos2Nat.inj_xI /= exprS !exprD expr0 mulr1 !mulrA. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound