proposition: Theorem prime_not_prime_S : forall n : nat, 2 < n -> prime n -> ~ prime (S n).
proof: Proof. intros n H (H1, H3); case (odd_or_even n); intros (n1, H2). absurd (n = 2). Contradict H; rewrite H; auto with arith. apply H3; auto with arith; exists n1; rewrite Nat.mul_comm; auto. red in |- *; intros (H4, H5); absurd (S n = 2). Contradict H; rewrite <- H; auto with arith. apply H5; auto with arith; exists (S n1); rewrite H2. lia. Qed.
imports: Coq(ArithRing Wf_nat Lia)