proposition: Lemma size_modnp_scale n k a v : size (modnp_scale n k a v) = k.
proof: Proof. by elim: k a v => //= k IH b v; rewrite IH. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound