proposition: Theorem check_postulate_correct : forall m : nat, check_postulate m = true -> forall n : nat, 2 <= n -> n <= m -> exists p : nat, prime p /\ n < p /\ p < 2 * n.
proof: Proof. intros m; elim m; simpl in |- *; auto. intros H n H0 H1; generalize H0; inversion H1; auto. intros H3; inversion H3. clear m; intros m; case m; clear m. intros H H0 n; case n; auto with arith. intros n1; case n1; auto with arith. intros n0 H1 H2; inversion H2. inversion H4. intros n H; (generalize (prime_between_correct (S (S (S n))) n); case (prime_between (S (S (S n))) n)). intros H0 H1 n0 H2 H3; inversion H3; auto with arith. case H0; auto; intros p1 (H5, (H6, H7)); (exists p1; repeat (split; auto with arith)). repeat rewrite <- plus_n_Sm || rewrite <- plus_n_O; auto with arith. intros; discriminate. Qed.
imports: Coq(Arith)