proposition: Theorem prime_div_prime: forall p q, prime p -> prime q -> (p | q) -> p = q.
proof: Proof. intros p q H H1 H2; assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. - intros H4; contradict Hp; subst; discriminate. - intros [H4| [H4 | H4]]; subst; auto. + contradict H; auto; apply not_prime_1. + contradict Hp; apply Zle_not_lt, (Z.opp_le_mono _ 0). now rewrite Z.opp_involutive; apply Z.lt_le_incl. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat