law add_right_cancel_iff

bend-mathlib@0.8.1.0 · nat.bend:3689

import Base

3689# Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k.
3690law add_right_cancel_iff:
3691  for a: Nat
3692  for b: Nat
3693  for k: Nat
3694  {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) : Bool}