Natfuel.halve: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend as Natfuel
Lines 98-121 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&start_line=98&end_line=121

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

# Knuth: b < 2^k and 2k + 1 <= f reach the end (r is a mod b, given)
def halve(+k: Nat, +f: Nat, +a: Nat, +b: Nat, +r: Nat, +hr: {Nat.mod(a, b) == r : Nat}, +hb: {Nat.is_lt(b, C.pow2(k)) == True{} : Bool}, +hf: {Nat.is_le(1n+Nat.double(k), f) == True{} : Bool}) -> {ends(f, a, b) == True{} : Bool}:
  match k f b r:
    case 0n _ 0n _:
      ends_zero(f, a)
    case 0n _ 1n+bp _:
      Empty.absurd({ends(f, a, 1n+bp) == True{} : Bool}, N.lt_zero_absurd(bp, hb))
    case 1n+j _ 0n _:
      ends_zero(f, a)
    case 1n+j 0n 1n+bp _:
      Empty.absurd({ends(0n, a, 1n+bp) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
    case 1n+j 1n 1n+bp _:
      Empty.absurd({ends(1n, a, 1n+bp) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
    case 1n+j 2n+ +h 1n+ +bp 0n:
      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 0n, hr) : {ends(1n+h, 1n+bp, _) == True{} : Bool}
      ends_zero(1n+h, 1n+bp)
    case 1n+ +j 2n+ +h 1n+ +bp 1n+ +rp:
      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 1n+rp, hr) : {ends(1n+h, 1n+bp, _) == True{} : Bool}
      +r2 = Nat.mod(1n+bp, 1n+rp)
      +h21 = NR.dm_lt(rp, 1n+bp)
      +hlt = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(a, 1n+bp), 1n+rp, hr, NR.dm_lt(bp, a))
      +hs = mod_le_sub(1n+bp, rp, N.lt_le(1n+rp, 1n+bp, hlt))
      +hb2 = halve2(1n+bp, 1n+rp, r2, C.pow2(j), hb, h21, hs)
      halve(j, h, 1n+rp, r2, Nat.mod(1n+rp, r2), {==}, hb2, hf)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&name=ends
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&name=ends_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&name=halve2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&name=mod_le_sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend&name=true_ne_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2