proposition: Theorem Zdiv_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a/b <= q.
proof: Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_upper_bound. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms