proposition: Lemma poly_modnp_scale n k a v : 0 < k -> 1 < n -> PolyZ n k (modnp_scale n k a v) = inZp a *: PolyZ n k v.
proof: Proof. move=> k_gt0 n_gt1; rewrite !PolyZE /= scaler_sumr. apply: eq_bigr => i _. rewrite scalerA; congr (_ *: _). elim: (k) (val i) (ltn_ord i) v => //= k1 IH [_ v|n1]; last first. rewrite ltnS => /IH HE v; rewrite [in inZp _]/= HE. by case: v => /=; rewrite ?nth_nil. case: v => [|x _] /=; rewrite ?(nth_nil, inZp0, add0r, addr0, add0n, addn0, mod0n) //=. by apply/val_eqP; rewrite /= Zp_cast // !muln0 !mod0n. by apply/val_eqP; rewrite /= Zp_cast // modn_mod modnMm. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound