PlanProofs.sub_balance: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
Lines 45-56 of bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&start_line=45&end_line=56

import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

def sub_balance(+a: Nat, +b: Nat) -> {Nat.add(Nat.sub(b, a), a) == Nat.add(Nat.sub(a, b), b) : Nat}:
  match a b:
    case 0n 0n:
      {==}
    case 0n 1n+q:
      Broadcast.add_zero(1n+q)
    case 1n+p 0n:
      Equal.sym(Nat, Nat.add(1n+p, 0n), 1n+p, Broadcast.add_zero(1n+p))
    case 1n+p 1n+q:
      %Broadcast.add_succ(Nat.sub(q, p), p) : {_ == Nat.add(Nat.sub(p, q), 1n+q) : Nat}
      %Broadcast.add_succ(Nat.sub(p, q), q) : {1n+Nat.add(Nat.sub(q, p), p) == _ : Nat}
      Equal.cong(Nat, Nat, value => 1n+value, Nat.add(Nat.sub(q, p), p), Nat.add(Nat.sub(p, q), q), sub_balance(p, q))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_zero