proposition: Lemma nonprime_sqrwitness : forall n : nat, n > 1 -> ~ Prime n -> exists d : nat, 1 < d /\ d * d <= n /\ Divides d n.
proof: Proof. intros. elim (nonprime_witness n). intro d. intros. elim (sqrdivbound n d). intro d'. intros. elim H2. intros. elim H4. intros. elim H6. intro. split with d'. split. rewrite H7. elim H1. tauto. split. assumption. rewrite H7. elim H1. tauto. intro. split with d'. split. apply (lt_n_nm_m_gt_1 d d'). rewrite H7. elim H1. tauto. split. assumption. assumption. elim H1. tauto. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list