law mul_le_mul_left

bend-mathlib@0.8.1.0 · nat.bend:2502

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

2502# Multiplying on the left preserves the order: a <= b implies k * a <= k * b.
2503law mul_le_mul_left:
2504  for a: Nat
2505  for b: Nat
2506  for k: Nat
2507  for h: le(a, b)
2508  le(Nat.mul(k, a), Nat.mul(k, b))

Uses (5)

Used by (5)