proposition: Theorem div_le_lower_bound: forall a b q, 0<b -> b*q <= a -> q <= a/b.
proof: Proof. intros. rewrite <- (div_mul q b) by order. apply div_le_mono; trivial. now rewrite mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv