proposition: Theorem bertrand_fun_aux_correct : forall n m : nat, match bertrand_fun_aux n m with | O => forall p : nat, n <= p /\ p <= n + m -> ~ prime p | S p => n <= S p /\ S p <= n + m /\ prime (S p) end.
proof: Proof. intros n m; generalize n; elim m; simpl in |- *; auto; clear n m. intros n; generalize (primeb_correct n); case (primeb n). case n; simpl in |- *; auto with arith. rewrite <- plus_n_O; intros H p (H1, H2); replace p with n; try apply Nat.le_antisymm; auto with arith. intros m Rec n. generalize (primeb_correct n); case (primeb n); auto with arith. case n; simpl in |- *; auto with arith. intros H; generalize (Rec (S n)); case (bertrand_fun_aux (S n) m); auto with arith. intros H0 p (H1, H2). case (proj1 (Nat.lt_eq_cases _ _) H1); auto with arith. intros H3; apply H0; auto with arith. split; auto with arith. rewrite Nat.add_succ_comm; auto. intros H3; rewrite <- H3; auto. intros n1 (H1, (H2, H3)); split; auto with arith; split; auto with arith. rewrite <- Nat.add_succ_comm; auto with arith. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)