proposition: Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)).
proof: Proof. intros. nzsimpl. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. destruct (mod_always_pos a b). { order. } rewrite abs_eq in *; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv