proposition: Theorem nonprime_primewitness : forall n : nat, n > 1 -> ~ Prime n -> exists d : nat, 1 < d /\ d * d <= n /\ Divides d n /\ Prime d.
proof: Proof. intro. apply (lt_wf_ind n). intros N IH. intros. elim (nonprime_sqrwitness N). intro x. intros. elim H1. intros. elim H3. intros. elim (primedec x). intros. split with x. split. assumption. split. assumption. split. assumption. assumption. intros. elim (IH x). intros. elim H7. intros. elim H9. intros. elim H11. intros. split with x0. split. assumption. split. apply le_trans with (x * x). apply le_trans with x. assumption. apply le_n_nn. assumption. split. apply div_trans with x. assumption. assumption. assumption. unfold lt in |- *. apply le_trans with (x * x). change (x < x * x) in |- *. apply sqr_ascend. assumption. assumption. assumption. assumption. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list