proposition: Theorem div_mul_le: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.
proof: Proof. intros a b c ? ? ?. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. apply mul_le_mono_nonneg_l; auto. apply mul_div_le; auto. Qed.
imports: NZAxioms NZMulOrder