proposition: Lemma mul_succ_quot_lt: forall a b, a<=0 -> b<0 -> b*(S (a÷b)) < a.
proof: Proof. intros. rewrite opp_lt_mono, <- mul_opp_l, <- quot_opp_opp by order. rewrite <- opp_nonneg_nonpos, <- opp_pos_neg in *. now apply mul_succ_quot_gt. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv