proposition: Theorem prime_div_Zpower_prime: forall n p q, 0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q.
proof: Proof. intros n p q Hp Hq; generalize p q Hq; pattern n; apply natlike_ind; auto; clear n p q Hp Hq. intros p q Hp Hq; rewrite Zpower_0_r. intros (r, H); subst. case (Zmult_interval p r); auto; try rewrite Zmult_comm. rewrite <- H; auto with zarith. apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. rewrite <- H; intros H1 H2; contradict H2; auto with zarith. intros n1 H Rec p q Hp Hq; try rewrite Zpower_Zsucc; auto with zarith; intros H1. case prime_mult with (2 := H1); auto. intros H2; apply prime_div_prime; auto. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic