proposition: Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}.
proof: Proof. destruct (Z.eq_dec a 0) as [Ha|Ha]. - destruct (Z.eq_dec b 0) as [Hb|Hb]. + left; subst; apply Z.divide_0_r. + right. subst. contradict Hb. now apply Z.divide_0_l. - destruct (Z.eq_dec (b mod a) 0). + left. now apply Z.mod_divide. + right. now rewrite <- Z.mod_divide. Defined.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat