proposition: Lemma PolyZE n k l : PolyZ n k l = \sum_(i < k) (inZp (nth 0%N l i)) *: 'X^i.
proof: Proof. apply/polyP=> i; rewrite coef_sum. case (leqP k i) => [kLi|iLk]. rewrite nth_default; last first. apply: leq_trans (size_Poly _) _. rewrite size_map size_take. by case: leqP => // /leq_trans->. rewrite big1 // => j _. rewrite coefZ coefXn. by case: ltngtP (leq_trans (ltn_ord j) kLi); rewrite ?mulr0. rewrite coef_Poly (bigD1 (Ordinal iLk)) //= big1 => [|j /eqP /val_eqP /= jDi]; last first. by rewrite coefZ coefXn eq_sym (negPf jDi) mulr0. rewrite addr0 coefZ coefXn eqxx mulr1. case: (leqP (size (take k l)) i) => [stLk|kLst]; last first. by rewrite (nth_map 0%N) // nth_take. rewrite nth_default ?size_map //. move: stLk; rewrite size_take; case: leqP => [_ slLi|]. by rewrite nth_default // inZp0. by case: ltngtP iLk. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound