proposition: Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.
proof: Proof. intros a b ? ?. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). - rewrite div_small; try split; order. - rewrite (div_mod a b) at 2 by order. apply lt_le_trans with (b*(a/b)). + rewrite <- (mul_1_l (a/b)) at 1. rewrite <- mul_lt_mono_pos_r; auto. apply div_str_pos; auto. + rewrite <- (add_0_r (b*(a/b))) at 1. rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed.
imports: NZAxioms NZMulOrder