law add_lt_add_iff_right_sym

bend-mathlib@0.8.1.0 · nat.bend:4618

import Base

4618# Adding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k, reversed to rewrite toward the simple side.
4619law add_lt_add_iff_right_sym:
4620  for a: Nat
4621  for b: Nat
4622  for k: Nat
4623  {Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) == Nat.is_lt(a, b) : Bool}