proposition: Lemma divdec : forall n d : nat, Divides d n \/ ~ Divides d n.
proof: Proof. intros. elim (divbdiv n d). intros. elim (bdivdec n d). left. apply (H0 H1). right. intro. apply H1. apply (H H2). Qed.
imports: ZArith Wf_nat lemmas natZ dec exp