proposition: Theorem div_le_upper_bound: forall a b q, 0<=a -> 0<b -> a <= b*q -> a/b <= q.
proof: Proof. intros a b q ? ? ?. rewrite (mul_le_mono_pos_l _ _ b) by order. apply le_trans with a; auto. apply mul_div_le; auto. Qed.
imports: NZAxioms NZMulOrder