proposition: Theorem not_prime_divide: forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p /\ (n | p).
proof: Proof. intros p Hp Hp1. case (prime_dec_aux p p); intros H1. - elim Hp1; constructor; auto. intros n (Hn1,Hn2). Z.le_elim Hn1; auto with zarith. subst n; constructor; auto with zarith. - case H1; intros n (Hn1,Hn2). destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]]. + exfalso. apply Z.gcd_eq_0_l in H. absurd (1 < n). * rewrite H; discriminate. * now intuition. + elim Hn2. red. rewrite <- H. apply Zgcd_is_gcd. + exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ]. apply Z.le_lt_trans with n; auto with zarith. * apply Z.divide_pos_le; auto with zarith. -- apply Z.lt_trans with 1; intuition. -- apply Z.gcd_divide_l. * intuition. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat