proposition: Theorem prime_2 : forall p : nat, prime p -> p = 2 \/ Nat.Odd p.
proof: Proof. intros p H. case (Nat.Even_or_Odd p); auto; intros H1; left. case H; intros H2 H3; apply H3; auto with arith. exists (Nat.div2 p); auto with arith. apply trans_equal with (Nat.double (Nat.div2 p)); auto with arith. rewrite <- even_double; auto. unfold Nat.double in |- *; ring. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)