proposition: Lemma bdivdec : forall n d : nat, bDivides d n \/ ~ bDivides d n.
proof: Proof. intros. unfold bDivides in |- *. apply ordec. apply eqdec. apply (exdec (fun q : nat => n = d * q) (S n)). intros. apply eqdec. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp