law sub_add

lawful-words@0.1.0.0 · proof_nat.bend:356

import Base

356# (x + y) - y = x.
357law sub_add:
358  for +x: Nat
359  for +y: Nat
360  {Nat.sub(Nat.add(x, y), y) == x : Nat}