proposition: Lemma size_modnp_add n k v1 v2 : size (modnp_add n k v1 v2) = k.
proof: Proof. by elim: k v1 v2 => //= k IH v1 v2; rewrite IH. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound