F64ratio.cz: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio.bend as F64ratio
Lines 32-45 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio.bend&start_line=32&end_line=45

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

def cz(+fuel: Nat, +w: WU.U64, +o: Bool, +ho: {X.odd(w) == o : Bool}) -> {F.ctz_go(fuel, w, o) == SF.tz(fuel, SW.value(w)) : Nat}:
  match fuel o:
    case 0n _:
      {==}
    case 1n+ +f True{}:
      +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), X.odd(w), True{}, Equal.sym(Bool, X.odd(w), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), WA.odd_value(w)), ho)
      Equal.sym(Nat, SF.tz(1n+f, SW.value(w)), 0n, Equal.cong(Bool, Nat, b => SF.pick(Nat, b, 0n, 1n+SF.tz(f, Nat.div(SW.value(w), 2n))), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), True{}, h))
    case 1n+ +f False{}:
      +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), X.odd(w), False{}, Equal.sym(Bool, X.odd(w), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), WA.odd_value(w)), ho)
      +e0 = Equal.cong(Bool, Nat, b => SF.pick(Nat, b, 0n, 1n+SF.tz(f, Nat.div(SW.value(w), 2n))), Nat.is_eq(Nat.mod(SW.value(w), 2n), 1n), False{}, h)
      +e1 = cz(f, X.half(w), X.odd(X.half(w)), {==})
      +e2 = Equal.cong(Nat, Nat, t => SF.tz(f, t), SW.value(X.half(w)), Nat.div(SW.value(w), 2n), WA.half_value(w))
      +e3 = Equal.trans(Nat, F.ctz_go(f, X.half(w), X.odd(X.half(w))), SF.tz(f, SW.value(X.half(w))), SF.tz(f, Nat.div(SW.value(w), 2n)), e1, e2)
      Equal.trans(Nat, 1n+F.ctz_go(f, X.half(w), X.odd(X.half(w))), 1n+SF.tz(f, Nat.div(SW.value(w), 2n)), SF.tz(1n+f, SW.value(w)), Equal.cong(Nat, Nat, t => 1n+t, F.ctz_go(f, X.half(w), X.odd(X.half(w))), SF.tz(f, Nat.div(SW.value(w), 2n)), e3), Equal.sym(Nat, SF.tz(1n+f, SW.value(w)), 1n+SF.tz(f, Nat.div(SW.value(w), 2n)), e0))

Uses (17):
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=half_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=odd_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=tz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=ctz_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=odd