law add_lt_add_iff_left

bend-mathlib@0.8.1.0 · nat.bend:2744

import Base

2744# Adding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b.
2745law add_lt_add_iff_left:
2746  for k: Nat
2747  for -a: Nat
2748  for -b: Nat
2749  {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) : Bool}