proposition: Lemma mul_quot_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a÷b) <= a.
proof: Proof. intros a b **. pos_or_neg b. - split. + apply mul_nonneg_nonneg; [|apply quot_pos]; order. + apply NZQuot.mul_div_le; order. - rewrite <- mul_opp_opp, <- quot_opp_r by order. split. + apply mul_nonneg_nonneg; [|apply quot_pos]; order. + apply NZQuot.mul_div_le; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv