proposition: Lemma size_modnp_pow n k p v : 0 < k -> size v = k -> size (modnp_pow n k p v) = k.
proof: Proof. move=> k_gt0 svE. elim: p => //= p spE; first by rewrite !size_modnp_mul. by rewrite size_modnp_mul. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound