proposition: Lemma divides_pow p n k : prime p -> divides p (n ^ k) -> divides p n.
proof: Proof. induction k. - cbn; intros H H0 % divides_1_inv; subst; exfalso; revert H; apply not_prime_1. - cbn; intros ? [ | ] % divides_mult_inv; eauto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)