law add_sub_cancel

bend-mathlib@0.8.1.0 · nat.bend:655

import Base

655# Adding then subtracting m cancels: (n + m) - m = n.
656law add_sub_cancel:
657  for n: Nat
658  for m: Nat
659  {Nat.sub(Nat.add(n, m), m) == n : Nat}