def k65536
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64div.bend:80
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64div
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
80def k65536(+one: Nat, +h1: {one == 1n : Nat}) -> {65536n == WD.sc(16n, one) : Nat}:
81 +o = oct(one, 13n, 8192n, 16384n, 24576n, 32768n, 40960n, 49152n, 57344n, 65536n, k8192(one, h1), {==}, {==}, {==}, {==}, {==}, {==}, {==})
82 Equal.trans(Nat, 65536n, WD.sc(3n, WD.sc(13n, one)), WD.sc(16n, one), o, WM.sc_sc(3n, 13n, one))