law add_left_cancel_iff

bend-mathlib@0.8.1.0 · nat.bend:3675

import Base

3675# Adding the same amount on the left does not change the equality test: a = b tests as k + a = k + b.
3676law add_left_cancel_iff:
3677  for k: Nat
3678  for -a: Nat
3679  for -b: Nat
3680  {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) : Bool}