law add_sub_cancel_left

bend-mathlib@0.8.1.0 · nat.bend:672

import Base

672# Adding then subtracting n cancels: (n + m) - n = m.
673law add_sub_cancel_left:
674  for n: Nat
675  for m: Nat
676  {Nat.sub(Nat.add(n, m), n) == m : Nat}