PROOF.rhp.w: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1487-1506 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=1487&end_line=1506

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

def rhp.w(
  -K: Data, -V: Data, single: Bool, -k: K, -v: V, -lk: K, -lv: V, +ll: O.OMap<K, V>,
  lh: O.OMap<K, V>, +hi: O.OMap<K, V>
) -> {Nat.add(Nat.add(W(K, V, ll), W(K, V, lh)), W(K, V, hi))
      == W(K, V, O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi)) : Nat}:
  match single lh:
    case True{} +lh:
      MNat.add_assoc(W(K, V, ll), W(K, V, lh), W(K, V, hi))
    case False{} O.OTip{}:
      MNat.add_assoc(W(K, V, ll), 1n, W(K, V, hi))
    case False{} O.OBin{s, mk, mv, +ml, +mh}:
      +l = W(K, V, hi)
      +x = W(K, V, mh)
      +y = W(K, V, ml)
      +b = W(K, V, ll)
      Ord.tr(Nat.add(Nat.add(b, Nat.add(y, x)), l), Nat.add(Nat.add(Nat.add(b, y), x), l),
        Nat.add(Nat.add(b, y), Nat.add(x, l)),
        Ord.cong_add(Nat.add(b, Nat.add(y, x)), Nat.add(Nat.add(b, y), x), l, l,
          Ord.sy(Nat.add(Nat.add(b, y), x), Nat.add(b, Nat.add(y, x)), MNat.add_assoc(b, y, x)), {==}),
        MNat.add_assoc(Nat.add(b, y), x, l))

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_hi.pick
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=add_assoc