proposition: Lemma poly_modnp_const n k v : 0 < k -> 1 < n -> PolyZ n k (modnp_const n k v) = v%:R%:P.
proof: Proof. rewrite Zp_nat. move=> k_gt0 n_gt1; apply/polyP => i. rewrite coefC /PolyZ -[in take _](prednK k_gt0) /= coef_cons; case: eqP => iE. by apply/val_eqP; rewrite /= Zp_cast // modn_mod. rewrite take_nseq //. case: (leqP k i) => iLk. have k1Li1 : k.-1 <= i.-1 by rewrite -ltnS !prednK //; case: (i) iE. by rewrite nth_default //= (leq_trans (size_Poly _)) // size_map size_nseq. have i1Lk1 : i.-1 < k.-1 by rewrite -ltnS !prednK //; case: (i) iE. by rewrite coef_Poly (nth_map 0%N) ?size_nseq // nth_nseq i1Lk1 // inZp0. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound