Fixbytes.dsplit: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes
Lines 242-251 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&start_line=242&end_line=251

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

def dsplit(+a: Nat, +b: Nat, +lo: Nat, +hi: Nat, +hlo: {C.fits(w8(a), lo) == True{} : Bool}) -> {SF.le_digits(Nat.add(a, b), Nat.add(lo, C.shift(w8(a), hi))) == C.append(Nat, SF.le_digits(a, lo), SF.le_digits(b, hi)) : List<&2, Nat>}:
  match a:
    case 0n:
      %Equal.sym(Nat, lo, 0n, fits0(lo, hlo)) : {SF.le_digits(b, Nat.add(_, hi)) == SF.le_digits(b, hi) : List<&2, Nat>}
      {==}
    case 1n+ +p:
      +Q = C.shift(w8(p), hi)
      +ets = Equal.trans(List<&2, Nat>, SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), SF.le_digits(Nat.add(p, b), Nat.add(C.high(8n, lo), Q)), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), Equal.cong(Nat, List<&2, Nat>, t => SF.le_digits(Nat.add(p, b), t), C.high(8n, Nat.add(lo, C.shift(8n, Q))), Nat.add(C.high(8n, lo), Q), WW.high_add_shift(8n, lo, Q)), dsplit(p, b, C.high(8n, lo), hi, SH.fits_high(8n, w8(p), lo, hlo)))
      %Equal.sym(Nat, C.shift(Nat.add(8n, w8(p)), hi), C.shift(8n, Q), WW.shift_comp(8n, w8(p), hi)) : {SF.le_digits(Nat.add(1n+p, b), Nat.add(lo, _)) == C.append(Nat, SF.le_digits(1n+p, lo), SF.le_digits(b, hi)) : List<&2, Nat>}
      con_eq(C.low(8n, Nat.add(lo, C.shift(8n, Q))), C.low(8n, lo), SF.le_digits(Nat.add(p, b), C.high(8n, Nat.add(lo, C.shift(8n, Q)))), C.append(Nat, SF.le_digits(p, C.high(8n, lo)), SF.le_digits(b, hi)), WW.low_add_shift(8n, lo, Q), ets)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=con_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=fits0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=w8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_add_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_add_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend&name=le_digits