proposition: Theorem primepropdiv : forall n : nat, n > 1 -> (forall q : nat, Prime q -> Divides q n -> q * q > n) -> Prime n.
proof: Proof. intros. elim (primedec n). intro. assumption. intros. elim (nonprime_primewitness n). intros. elim H2. intros. elim H4. intros. elim H6. intros. elim (le_not_lt (x * x) n). assumption. unfold gt in H0. apply H0. assumption. assumption. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list