proposition: Lemma size_modnp_Xn n k v : 0 < k -> size (modnp_Xn n k v) = k.
proof: Proof. move=> k_gt0; rewrite /= size_cat size_nseq /= size_nseq. by rewrite addnC addSn subnK ?prednK // -ltnS prednK // ltn_mod. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound