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