law lt_sub_iff_add_lt

bend-mathlib@0.8.1.0 · nat.bend:1804

import Base

1804# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.
1805law lt_sub_iff_add_lt:
1806  for a: Nat
1807  for b: Nat
1808  for c: Nat
1809  {Nat.is_lt(a, Nat.sub(c, b)) == Nat.is_lt(Nat.add(b, a), c) : Bool}