U64div.expand: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div
Lines 109-120 of bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend&start_line=109&end_line=120

import Base
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/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

# 2^8 (2^12 (2^12 h + a) + b) + c == ((2^20 a + 2^8 b) + c) + 2^32 h
def expand(+h: Nat, +a: Nat, +b: Nat, +c: Nat) -> {Nat.add(WD.sc(8n, Nat.add(WD.sc(12n, Nat.add(WD.sc(12n, h), a)), b)), c) == Nat.add(Nat.add(Nat.add(WD.sc(20n, a), WD.sc(8n, b)), c), WD.sc(32n, h)) : Nat}:
  +rhs = Nat.add(Nat.add(Nat.add(WD.sc(20n, a), WD.sc(8n, b)), c), WD.sc(32n, h))
  +x = WD.sc(32n, h)
  +y = WD.sc(20n, a)
  +z = WD.sc(8n, b)
  %A.sc_add(12n, WD.sc(12n, h), a) : {Nat.add(WD.sc(8n, Nat.add(_, b)), c) == rhs : Nat}
  %A.sc_add(8n, Nat.add(WD.sc(12n, WD.sc(12n, h)), WD.sc(12n, a)), b) : {Nat.add(_, c) == rhs : Nat}
  %A.sc_add(8n, WD.sc(12n, WD.sc(12n, h)), WD.sc(12n, a)) : {Nat.add(Nat.add(_, z), c) == rhs : Nat}
  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(x, y), z), c), Nat.add(Nat.add(x, Nat.add(y, z)), c), rhs,
    Equal.cong(Nat, Nat, w => Nat.add(w, c), Nat.add(Nat.add(x, y), z), Nat.add(x, Nat.add(y, z)), N.add_assoc(x, y, z)),
    Equal.trans(Nat, Nat.add(Nat.add(x, Nat.add(y, z)), c), Nat.add(x, Nat.add(Nat.add(y, z), c)), rhs, N.add_assoc(x, Nat.add(y, z), c), N.add_comm(x, Nat.add(Nat.add(y, z), c))))

Uses (8):
  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.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=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=sc_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc