~/jendhub

law lt_add_right

bend-mathlib@0.8.1.0 · nat.bend:2670

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

2670# Adding on the right keeps a strict bound: n < m implies n < m + k.
2671law lt_add_right:
2672  for n: Nat
2673  for m: Nat
2674  for -k: Nat
2675  for h: lt(n, m)
2676  lt(n, Nat.add(m, k))

Uses (5)

Used by (0)

No other definition uses this definition.