proposition: Lemma size_modnp_mul n k v1 v2 : 0 < k -> size (modnp_mul n k v1 v2) = k.
proof: Proof. move=> k_gt0. case: v2 => [|a v4 /=]; first by rewrite size_modnp_const. by rewrite size_modnp_add. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound