law sub_add_l

lawful-words@0.1.0.0 · proof_nat.bend:372

import Base

372# (y + x) - y = x.
373law sub_add_l:
374  for +y: Nat
375  for +x: Nat
376  {Nat.sub(Nat.add(y, x), y) == x : Nat}