law lt_sub_iff_add_lt_sym

bend-mathlib@0.8.1.0 · nat.bend:4341

import Base

4341# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
4342law lt_sub_iff_add_lt_sym:
4343  for a: Nat
4344  for b: Nat
4345  for c: Nat
4346  {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}