law add_left_cancel_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4855

import Base

4855# Adding the same amount on the left does not change the equality test: a = b tests as k + a = k + b, reversed to rewrite toward the simple side.
4856law add_left_cancel_iff_sym:
4857  for k: Nat
4858  for -a: Nat
4859  for -b: Nat
4860  {Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) == Nat.is_eq(a, b) : Bool}