W64div.k65536: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64div
Lines 80-82 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend&start_line=80&end_line=82

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as WM

def k65536(+one: Nat, +h1: {one == 1n : Nat}) -> {65536n == WD.sc(16n, one) : Nat}:
  +o = oct(one, 13n, 8192n, 16384n, 24576n, 32768n, 40960n, 49152n, 57344n, 65536n, k8192(one, h1), {==}, {==}, {==}, {==}, {==}, {==}, {==})
  Equal.trans(Nat, 65536n, WD.sc(3n, WD.sc(13n, one)), WD.sc(16n, one), o, WM.sc_sc(3n, 13n, one))

Uses (6):
  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=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend&name=k8192
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend&name=oct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=sc_sc