proposition: Theorem postulate_dec : forall n : nat, {(exists p : nat, prime p /\ n < p /\ p < 2 * n)} + {(forall p : nat, n < p -> p < 2 * n -> ~ prime p)}.
proof: Proof. intros n; case n. right; simpl in |- *; intros p H1 H2; inversion H2. intros n1; case n1. right; simpl in |- *; intros p H1; inversion H1; auto with arith. intros H2; Contradict H2; auto with arith. intros H2; inversion H2; auto with arith. inversion H4; auto. inversion H6. intros n2; generalize (prime_between_correct (S (S (S n2))) n2); case (prime_between (S (S (S n2))) n2). intros H0; left; case H0; intros p (H1, (H2, H3)); exists p; repeat (split; auto with arith). simpl in |- *; repeat rewrite <- plus_n_Sm || rewrite <- plus_n_O; auto with arith. intros H0; right; intros p H1 H2; apply H0; auto with arith. generalize H2; simpl in |- *; repeat rewrite <- plus_n_Sm || rewrite <- plus_n_O; auto with arith. Qed.
imports: Coq(Arith)