proposition: Lemma poly_modnp_mul n k v1 v2 : 0 < k -> 1 < n -> size v2 = k -> PolyZ n k (modnp_mul n k v1 v2) = rmodp (PolyZ n k v1 * PolyZ n k v2) ('X^k - 1).
proof: Proof. move=> k_gt0 n_gt1 sv2E. have : size v2 <= k by rewrite sv2E. have xnM := monic_Xn_sub_1 [ringType of 'Z_n] k_gt0. elim: {sv2E}v2 => /= [|a v4 IH sv4E]. by rewrite poly_modnp_const // PolyZ_nil mulr0 rmod0p Zp_nat inZp0. rewrite poly_modnp_add // poly_modnp_scale //. rewrite poly_modnp_mulX ?size_modnp_mul // IH; last by apply: ltnW. rewrite PolyZ_cons // mulrDr rmodpD // rmodp_mulmr // mulrCA. congr (_ + _). rewrite -mulr_algr -Zp_nat scaler_nat. rewrite rmodp_small // size_Xn_sub_1 //. apply: leq_trans (size_mul_leq _ _) _. rewrite -polyC_natr size_polyC. apply: leq_trans (size_PolyZ n k v1). case: eqP=> _; first by rewrite addn0 leq_pred. by rewrite addn1. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound