proposition: Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c.
proof: Proof. intros a b c **. pos_or_neg a. - apply NZQuot.div_le_mono; auto. - pos_or_neg b. + apply le_trans with 0. * rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order. apply quot_pos; order. * apply quot_pos; order. + rewrite opp_le_mono in *. rewrite <- 2 quot_opp_l by order. apply NZQuot.div_le_mono; intuition; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv