proposition: Lemma mul_succ_div_lt: forall a b, b<0 -> b*(S (a/b)) < a.
proof: Proof. intros. rewrite <- div_opp_opp, opp_lt_mono, <-mul_opp_l by order. apply mul_succ_div_gt. now rewrite opp_pos_neg. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv