proposition: Lemma size_PolyZ n k l : size (PolyZ n k l) <= k.
proof: Proof. apply: leq_trans (size_Poly _) _. by rewrite size_map size_take; case: leqP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound