proposition: Lemma mul_quot_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a÷b) <= 0.
proof: Proof. intros a b **. rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. destruct (mul_quot_le (-a) b); tauto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv