law add_sub_add_right

bend-mathlib@0.8.1.0 · nat.bend:2286

import Base

2286# A common right summand cancels in a difference: (n + k) - (m + k) = n - m.
2287law add_sub_add_right:
2288  for n: Nat
2289  for k: Nat
2290  for m: Nat
2291  {Nat.sub(Nat.add(n, k), Nat.add(m, k)) == Nat.sub(n, m) : Nat}