~/jendhub

law lt_sub_of_add_lt

bend-mathlib@0.8.1.0 · nat.bend:2998

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

2998# A strict bound on a sum bounds a difference: a + b < c implies a < c - b.
2999law lt_sub_of_add_lt:
3000  for a: Nat
3001  for b: Nat
3002  for c: Nat
3003  for h: lt(Nat.add(a, b), c)
3004  lt(a, Nat.sub(c, b))

Uses (9)

Used by (1)