proposition: Theorem primeb_correct : forall n : nat, if primeb n then prime n else ~ prime n.
proof: Proof. intros n; case n; auto with arith. simpl in |- *; auto with arith. intros n1; case n1; auto with arith. simpl in |- *; auto with arith. intros n2; generalize (max_div_prop1 (S (S n2))); generalize (max_div_prop2 (S (S n2))); generalize (max_div_prop3 (S (S n2))); unfold primeb in |- *; case (max_div (S (S n2))). intros H' H (x, H0); rewrite Nat.mul_comm in H0; discriminate. intros n3; case n3. intros H' H H0; split; auto with arith. intros b; case b. intros (x, H1); rewrite Nat.mul_comm in H1; discriminate. intros n0 H1 H2; case (proj1 (Nat.lt_eq_cases (S n0) (S (S n2)))); auto. apply divides_le; auto with arith. intros H3; case (H (S n0)); auto with arith. generalize H2; case n0; simpl in |- *; auto with arith. intros H4; case H4; auto. intros n0 H H0 H1; red in |- *; intros (H2, H4). absurd (S (S n2) <= S (S n0)); auto with arith. rewrite (H4 (S (S n0))); auto. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)