proposition: Theorem Zdiv_lt_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_lt_upper_bound. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms