law add_sub_cancel_left_sym

bend-mathlib@0.8.1.0 · nat.bend:4046

import Base

4046# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
4047law add_sub_cancel_left_sym:
4048  for n: Nat
4049  for m: Nat
4050  {m == Nat.sub(Nat.add(n, m), n) : Nat}