law add_le_add_left

bend-mathlib@0.8.1.0 · nat.bend:1486

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

import Base

1486# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1487law add_le_add_left:
1488  for -a: Nat
1489  for -b: Nat
1490  for k: Nat
1491  for h: le(a, b)
1492  le(Nat.add(k, a), Nat.add(k, b))

Uses (3)

Used by (4)