PROOF.rlp.w: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1462-1485 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=1462&end_line=1485

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat
import bend-kit-collections@0.1.4.1/omap.bend as O
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

# Balancing keeps the weight.
def rlp.w(
  -K: Data, -V: Data, single: Bool, -k: K, -v: V, +lo: O.OMap<K, V>, -hk: K, -hv: V,
  hl: O.OMap<K, V>, +hh: O.OMap<K, V>
) -> {Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh)))
      == W(K, V, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh)) : Nat}:
  match single hl:
    case True{} +hl:
      Ord.sy(Nat.add(Nat.add(W(K, V, lo), W(K, V, hl)), W(K, V, hh)),
        Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh))),
        MNat.add_assoc(W(K, V, lo), W(K, V, hl), W(K, V, hh)))
    case False{} O.OTip{}:
      Ord.sy(Nat.add(Nat.add(W(K, V, lo), 1n), W(K, V, hh)), Nat.add(W(K, V, lo), Nat.add(1n, W(K, V, hh))),
        MNat.add_assoc(W(K, V, lo), 1n, W(K, V, hh)))
    case False{} O.OBin{s, mk, mv, +ml, +mh}:
      +l = W(K, V, lo)
      +x = W(K, V, ml)
      +y = W(K, V, mh)
      +b = W(K, V, hh)
      Ord.tr(Nat.add(l, Nat.add(Nat.add(x, y), b)), Nat.add(l, Nat.add(x, Nat.add(y, b))),
        Nat.add(Nat.add(l, x), Nat.add(y, b)),
        Ord.cong_add(l, l, Nat.add(Nat.add(x, y), b), Nat.add(x, Nat.add(y, b)), {==}, MNat.add_assoc(x, y, b)),
        Ord.sy(Nat.add(Nat.add(l, x), Nat.add(y, b)), Nat.add(l, Nat.add(x, Nat.add(y, b))),
          MNat.add_assoc(l, x, Nat.add(y, b))))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=bend-kit-collections@0.1.4.1/PROOF.bend&name=W
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=cong_add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=sy
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=tr
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.rot_lo.pick
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_assoc