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