proposition: Theorem quot_le_upper_bound: forall a b q, 0<b -> a <= b*q -> a÷b <= q.
proof: Proof. intros a b q **. rewrite <- (quot_mul q b) by order. apply quot_le_mono; trivial. now rewrite mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv