~/jendhub

law add_le_add_right

bend-mathlib@0.8.1.0 · nat.bend:1501

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

1501# Adding on the right preserves the order: a <= b implies a + k <= b + k.
1502law add_le_add_right:
1503  for +a: Nat
1504  for +b: Nat
1505  for +k: Nat
1506  for h: le(a, b)
1507  le(Nat.add(a, k), Nat.add(b, k))

Uses (5)

Used by (1)