proposition: Theorem prime_def1 : forall n : nat, 1 < n -> (forall p : nat, prime p -> p * p <= n -> ~ divides p n) -> prime n.
proof: Proof. intros n H H0; split; auto with arith. contradict H; rewrite H; auto with arith. intros b (x, H1) H2. case (Nat.le_gt_cases x b); intros H3. case (Nat.le_gt_cases x 1); intros H4. case (proj1 (Nat.lt_eq_cases _ _) H4); intros H5. case (proj1 (Nat.lt_eq_cases x 0)); auto with arith; intros H6. inversion H6. contradict H; rewrite H1; rewrite H6; auto with arith. rewrite H1; rewrite H5; auto with arith. case (divides_prime_divides x); auto with arith. intros y (H5, H6); case (H0 y); auto with arith. cut (y <= x); [ intros H7 | apply divides_le ]; auto. apply Nat.le_trans with (x * y); auto with arith. apply le_mult; auto with arith. rewrite H1; auto with arith. apply le_mult; auto with arith. apply Nat.le_trans with (1 := H7); auto. contradict H4; rewrite H4; auto with arith. apply divides_trans with (1 := H6); exists b; auto with arith. rewrite Nat.mul_comm; auto. case (divides_prime_divides b); auto with arith. generalize H2 H; rewrite H1; case b; auto with arith. intros H4; rewrite Nat.mul_comm; intros H5; contradict H5; auto with arith. intros n1; case n1; auto with arith. intros H4; case H4; auto with arith. intros y (H5, H6); case (H0 y); auto with arith. cut (y <= b); [ intros H7 | apply divides_le ]; auto. apply Nat.le_trans with (x * y); auto with arith. apply le_mult; auto with arith. apply Nat.le_trans with (1 := H7); auto with arith. rewrite H1; auto with arith. contradict H; rewrite H1; rewrite H; rewrite Nat.mul_comm; auto with arith. apply divides_trans with (1 := H6). exists x; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)