proposition: Theorem prime_power_prime p q n : 0 <= n -> prime p -> prime q -> (p | q^n) -> p = q.
proof: Proof. intros Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn. - simpl; intros. assert (2<=p) by (apply prime_ge_2; auto). assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). lia. - intros n Hn Rec. rewrite Z.pow_succ_r by trivial. intros H. assert (2<=p) by (apply prime_ge_2; auto). assert (2<=q) by (apply prime_ge_2; auto). destruct prime_mult with (2 := H); auto. apply prime_div_prime; auto. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower