proposition: Lemma PolyZ_nil n k : PolyZ n k [::] = 0.
proof: Proof. by rewrite PolyZE big1 // => i _; rewrite nth_nil inZp0 scale0r. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound