law add_right_cancel_iff_sym

bend-mathlib@0.8.1.0 · nat.bend:4865

import Base

4865# Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k, reversed to rewrite toward the simple side.
4866law add_right_cancel_iff_sym:
4867  for a: Nat
4868  for b: Nat
4869  for k: Nat
4870  {Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) == Nat.is_eq(a, b) : Bool}