proposition: Theorem Zquot_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q.
proof: Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_lt_upper_bound. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms