def sub_balance

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:45

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

45def sub_balance(+a: Nat, +b: Nat) -> {Nat.add(Nat.sub(b, a), a) == Nat.add(Nat.sub(a, b), b) : Nat}:
46  match a b:
47    case 0n 0n:
48      {==}
49    case 0n 1n+q:
50      Broadcast.add_zero(1n+q)
51    case 1n+p 0n:
52      Equal.sym(Nat, Nat.add(1n+p, 0n), 1n+p, Broadcast.add_zero(1n+p))
53    case 1n+p 1n+q:
54      %Broadcast.add_succ(Nat.sub(q, p), p) : {_ == Nat.add(Nat.sub(p, q), 1n+q) : Nat}
55      %Broadcast.add_succ(Nat.sub(p, q), q) : {1n+Nat.add(Nat.sub(q, p), p) == _ : Nat}
56      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))