law mul_le_mul_right

bend-mathlib@0.8.1.0 · nat.bend:1834

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

import Base

1834# Multiplying on the right preserves the order: a <= b implies a * k <= b * k.
1835law mul_le_mul_right:
1836  for +a: Nat
1837  for +b: Nat
1838  for +k: Nat
1839  for h: le(a, b)
1840  le(Nat.mul(a, k), Nat.mul(b, k))

Uses (12)

Used by (5)