proposition: Lemma zdivdec : forall x d : Z, ZDivides d x \/ ~ ZDivides d x.
proof: Proof. intros. elim (divdec (Z.abs_nat x) (Z.abs_nat d)). left. apply divzdiv. assumption. right. intro. apply H. apply zdivdiv. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp