proposition: Lemma poly_modnp_eq n k v1 v2 : 0 < k -> 1 < n -> (modnp_eq n k v1 v2) = (PolyZ n k v1 == PolyZ n k v2).
proof: Proof. move=> k_gt0 n_gt1; rewrite !PolyZE. elim: (k) v1 v2 => [|k1 IH] v1 v2; first by rewrite !big1 ?eqxx // => [[]|[]]. rewrite /= IH -!(poly_def _ (fun i => inZp (nth 0%nat _ i))). apply/andP/eqP=> [[/eqP hE /eqP/polyP pE]| /polyP pE]. apply/polyP=> i; rewrite !coef_poly; case: leqP => //. case: i => [_|i]. by (case: (v1) hE; case: (v2)) => //= [a _ aE|a _ aE|a _ b _ aE]; apply/val_eqP/eqP; rewrite /= Zp_cast. rewrite ltnS => iLk1. have := pE i; rewrite !coef_poly iLk1. by (case: (v1); case: (v2)) => //= [_ l <-|_ l ->]; rewrite nth_nil. split; apply/eqP. have := pE 0%nat; rewrite !coef_poly ltnS leq0n. by (case: (v1); case: (v2)) => //= [a _ |a _|a _ b _] /val_eqP/eqP/=; rewrite Zp_cast. apply/polyP=> i; rewrite !coef_poly; case: leqP => // iLk1. have := pE i.+1; rewrite !coef_poly ltnS iLk1. by (case: (v1); case: (v2)) => //= [_ l|_ l]; rewrite nth_nil. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound