def add_sub_cancel

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:263

import Base

263def add_sub_cancel(+a: Nat, +b: Nat) -> {Nat.sub(Nat.add(a, b), a) == b : Nat}:
264  match a b:
265    case 0n 0n:
266      {==}
267    case 0n 1n+q:
268      {==}
269    case 1n+p _:
270      add_sub_cancel(p, b)