proposition: Theorem div_lt_upper_bound: forall a b q, 0<b -> a < b*q -> a/b < q.
proof: Proof. intros. rewrite (mul_lt_mono_pos_l b) by trivial. apply le_lt_trans with a; trivial. apply mul_div_le; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv