proposition: Lemma primedec : forall n : nat, Prime n \/ ~ Prime n.
proof: Proof. intro. elim (primebprime n). intros. elim (bprimedec n). left. apply (H0 H1). right. intro. apply H1. apply (H H2). Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list