law add_lt_add_iff_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4608

import Base

4608# Adding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b, reversed to rewrite toward the simple side.
4609law add_lt_add_iff_left_sym:
4610  for k: Nat
4611  for -a: Nat
4612  for -b: Nat
4613  {Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) == Nat.is_lt(a, b) : Bool}