proposition: Lemma poly_modnp_add n k v1 v2 : 0 < k -> 1 < n -> PolyZ n k (modnp_add n k v1 v2) = PolyZ n k v1 + PolyZ n k v2.
proof: Proof. move=> k_gt0 n_gt1; rewrite !PolyZE -big_split /=. apply: eq_bigr => i _. rewrite -scalerDl; congr (_ *: _). elim: (k) (val i) (ltn_ord i) v1 v2 => //= k1 IH [_ v1 v2|n1]; last first. rewrite ltnS => /IH HE v1 v2; rewrite [in inZp _]/= HE. by case: v1 => /=; case: v2 => /=; rewrite ?nth_nil. case: v1 => [|x _] /=; (case: v2 => [|y _] /=); rewrite ?(nth_nil, inZp0, add0r, addr0, add0n, addn0, mod0n) //=. - by apply/val_eqP; rewrite /= Zp_cast // modn_mod. - by apply/val_eqP; rewrite /= Zp_cast // modn_mod. by apply/val_eqP; rewrite /= Zp_cast // modn_mod modnDm. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound