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