proposition: Lemma mul_pred_div_gt: forall a b, b<0 -> a < b*(P (a/b)).
proof: Proof. intros a b Hb. rewrite mul_pred_r, <- add_opp_r. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. destruct (mod_always_pos a b). { order. } rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv