proposition: Theorem prime_div_prime : forall p n : nat, p < n -> prime p -> divides p n -> ~ prime n.
proof: Proof. intros p n H1 H2 H3; red in |- *; intros (H4, H5). Contradict H1; rewrite (H5 p); auto with arith. Contradict H2; rewrite H2; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)