proposition: Lemma size_modnp_mulX n k v : 0 < k -> size v = k -> size (modnp_mulX n k v) = k.
proof: Proof. by move=> k_gt0 vsEk; rewrite size_belast. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound