proposition: Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b.
proof: Proof. intros H Hb. rewrite <- Z.divide_abs_l, <- Z.divide_abs_r in H. apply Z.abs_pos in Hb. now apply Z.divide_pos_le. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat