proposition: Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
proof: Proof. intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. destruct (mod_bound_pos a b); auto. Qed.
imports: NZAxioms NZMulOrder