proposition: Lemma PolyZ_cons n k a v : 0 < k -> 1 < n -> size v < k -> PolyZ n k (a :: v) = a%:R + 'X * PolyZ n k v :> {poly 'Z_n}.
proof: Proof. move=> k_gt0 n_gt1 svE; rewrite !PolyZE. rewrite -(prednK k_gt0) big_ord_recl /=; congr (_ + _). by rewrite expr0 /= -Zp_nat scaler_nat. rewrite [in RHS]big_ord_recr /= nth_default ?svE; last first. by rewrite -ltnS prednK. rewrite inZp0 scale0r addr0. rewrite mulr_sumr; apply: eq_bigr => i _. by rewrite -scalerAr exprS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound