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