proposition: Lemma Prime_dec (n: nat) : Prime n \/ ~ Prime n.
proof: Proof. destruct (prime_dec (Z.of_nat n)). + left. apply prime_Prime. auto. + right. intro. apply n0. apply Prime_prime. auto. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow