law add_lt_add_iff_right

bend-mathlib@0.8.1.0 · nat.bend:2758

import Base

2758# Adding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k.
2759law add_lt_add_iff_right:
2760  for a: Nat
2761  for b: Nat
2762  for k: Nat
2763  {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) : Bool}