proposition: Lemma nonprime_witness : forall n : nat, n > 1 -> ~ Prime n -> exists d : nat, 1 < d /\ d < n /\ Divides d n.
proof: Proof. intro n. case n. intro. elim (lt_n_O 1). assumption. intro n1. case n1. intro. elim (lt_irrefl 1). assumption. intro n2. intros. elim (decDeMorgan (S (S n2)) (fun d : nat => 1 < d /\ Divides d (S (S n2)))). intros. elim H2. intros. split with x. elim H3. intros. elim H5. intros. split. assumption. split. assumption. assumption. intro. apply H0. unfold Prime in |- *. split. assumption. intro q. case q. intro. unfold Divides in H4. elim H4. simpl in |- *. intros. discriminate H5. intro q1. case q1. left. reflexivity. intro q2. intros. right. elim (le_lt_or_eq (S (S q2)) (S (S n2))). intros. elim (H3 (S (S q2))). assumption. split. apply lt_n_S. apply lt_O_Sn. assumption. intros. assumption. apply div_le1. assumption. intros. apply anddec. apply ltdec. apply divdec. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list