proposition: Lemma bprimedec : forall n : nat, bPrime n \/ ~ bPrime n.
proof: Proof. unfold bPrime in |- *. intros. apply anddec. apply gtdec. apply (alldec (fun q : nat => Divides q n -> q = 1 \/ q = n) (S n)). intros. apply impdec. apply divdec. apply ordec. apply eqdec. apply eqdec. Qed.
imports: ZArith Wf_nat lemmas natZ dec divides modulo list