proposition: Lemma zdivdiv : forall a b : Z, ZDivides a b -> Divides (Z.abs_nat a) (Z.abs_nat b).
proof: Proof. intros. elim H. intros d Hd. exists (Z.abs_nat d). rewrite Hd. apply abs_mult. Qed.
imports: ZArith Wf_nat lemmas natZ dec exp