Fixgen.wsub: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as Fixgen
Lines 76-99 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend&start_line=76&end_line=99

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# d == x - y + 2^k modulo 2^k: its low part plus y is x, plus 2^k when x < y
def wsub(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +y: Nat, +d: Nat, +e: {Nat.add(d, y) == Nat.add(x, C.shift(k, one)) : Nat}, +hx: {C.fits(k, x) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(x, y) == c : Bool}) -> {Nat.add(C.low(k, d), y) == Nat.add(x, C.shift(k, SF.bn(c))) : Nat}:
  match c:
    case True{}:
      +S = C.shift(k, one)
      +g1 = N.lt_add_r2(x, y, S, hc)
      +g2 = Equal.trans(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(y, S)), Nat.is_lt(Nat.add(x, S), Nat.add(y, S)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(y, S)), Nat.add(d, y), Nat.add(x, S), e), g1)
      +g3 = Equal.trans(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), Nat.is_lt(Nat.add(d, y), Nat.add(y, S)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.add(d, y), t), Nat.add(S, y), Nat.add(y, S), N.add_comm(S, y)), g2)
      +g4 = Equal.trans(Bool, Nat.is_lt(d, S), Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(d, y), Nat.add(S, y)), Nat.is_lt(d, S), WW.lt_cancel_r(d, S, y)), g3)
      +hf = WW.fits_one(k, one, h1, d, g4)
      %h1 : {Nat.add(C.low(k, d), y) == Nat.add(x, C.shift(k, _)) : Nat}
      %Equal.sym(Nat, C.low(k, d), d, WW.low_fit(k, d, hf)) : {Nat.add(_, y) == Nat.add(x, C.shift(k, one)) : Nat}
      e
    case False{}:
      +S = C.shift(k, one)
      +z = Nat.sub(x, y)
      +hle = N.not_lt_le(x, y, hc)
      +exz = N.sub_add(x, y, hle)
      +e1 = Equal.trans(Nat, Nat.add(Nat.add(z, S), y), Nat.add(Nat.add(y, z), S), Nat.add(x, S), rot3(z, S, y), Equal.cong(Nat, Nat, t => Nat.add(t, S), Nat.add(y, z), x, exz))
      +ed = add_cancel_r(d, Nat.add(z, S), y, Equal.trans(Nat, Nat.add(d, y), Nat.add(x, S), Nat.add(Nat.add(z, S), y), e, Equal.sym(Nat, Nat.add(Nat.add(z, S), y), Nat.add(x, S), e1)))
      +el = Equal.trans(Nat, C.low(k, d), C.low(k, Nat.add(z, S)), z, Equal.cong(Nat, Nat, t => C.low(k, t), d, Nat.add(z, S), ed), WW.low_u(k, z, one, fits_sub(k, x, y, hx)))
      %Equal.sym(Nat, C.low(k, d), z, el) : {Nat.add(_, y) == Nat.add(x, C.shift(k, 0n)) : Nat}
      %Equal.sym(Nat, C.shift(k, 0n), 0n, WW.shift_zero(k)) : {Nat.add(z, y) == Nat.add(x, _) : Nat}
      Equal.trans(Nat, Nat.add(z, y), x, Nat.add(x, 0n), Equal.trans(Nat, Nat.add(z, y), Nat.add(y, z), x, N.add_comm(z, y), exz), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)))

Uses (25):
  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=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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend&name=add_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend&name=fits_sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend&name=rot3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=fits_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_zero
  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=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=bn