proposition: Theorem divides_prime_divides : forall n : nat, 1 < n -> exists p : nat, prime p /\ divides p n.
proof: Proof. intros n; pattern n in |- *; apply lt_wf_ind. clear n; intros n Rec H1. case (Nat.le_gt_cases (max_div n) 1); intros H2. exists n; split; auto with arith. split; auto with arith. contradict H1; rewrite H1; auto with arith. intros b H H0. cut (0 <> b); [ intros H4 | idtac ]. case (proj1 (Nat.lt_eq_cases b n)); auto with arith. apply divides_le; auto with arith. contradict H1; rewrite H1; auto with arith. intros H3; contradict H. apply max_div_prop2; auto with arith. apply Nat.le_lt_trans with (1 := H2); auto with arith. generalize H0 H4; case b; auto with arith. intros HH1 HH2; case HH2; auto. intros n1; case n1; auto with arith. intros HH1; case HH1; auto with arith. contradict H1; case H; intros x H3; rewrite H3; rewrite <- H1; rewrite Nat.mul_comm; auto with arith. case (Rec (max_div n)); auto with arith. apply max_div_prop3; auto with arith. intros x (H3, H4); exists x; split; auto. apply divides_trans with (1 := H4). apply max_div_prop1; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)