W64mul.expand16: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul
Lines 130-146 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&start_line=130&end_line=146

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/lib/lemmas/proofs/nat_algebra.bend as NA

# (al + 2^16 ah)(bl + 2^16 bh) == (al bl + 2^16 al bh) + (2^16 ah bl + 2^32 ah bh)
def expand16(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat) -> {Nat.mul(Nat.add(al, WD.sc(16n, ah)), Nat.add(bl, WD.sc(16n, bh))) == Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))) : Nat}:
  +b = Nat.add(bl, WD.sc(16n, bh))
  +sa = WD.sc(16n, ah)
  +sb = WD.sc(16n, bh)
  +e6 = Equal.trans(Nat, Nat.mul(sa, sb), WD.sc(16n, Nat.mul(ah, sb)), WD.sc(32n, Nat.mul(ah, bh)), mul_sc_l(16n, ah, sb), Equal.trans(Nat, WD.sc(16n, Nat.mul(ah, sb)), WD.sc(16n, WD.sc(16n, Nat.mul(ah, bh))), WD.sc(32n, Nat.mul(ah, bh)), cong_sc(16n, Nat.mul(ah, sb), WD.sc(16n, Nat.mul(ah, bh)), mul_sc_r(16n, ah, bh)), sc_sc(16n, 16n, Nat.mul(ah, bh))))
  +l1 = Nat.add(Nat.mul(al, b), Nat.mul(sa, b))
  +l2 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b))
  +l3 = Nat.add(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
  +l4 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)))
  +l5 = Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)))
  Equal.trans(Nat, Nat.mul(Nat.add(al, sa), b), l1, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), NA.mul_add_right(al, sa, b),
    Equal.trans(Nat, l1, l2, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.mul(al, b), Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), NA.mul_add_left(al, bl, sb)),
      Equal.trans(Nat, l2, l3, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.mul(sa, b), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), NA.mul_add_left(sa, bl, sb)),
        Equal.trans(Nat, l3, l4, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_l(Nat.add(Nat.mul(al, bl), Nat.mul(al, sb)), Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), cong_r(Nat.mul(al, bl), Nat.mul(al, sb), WD.sc(16n, Nat.mul(al, bh)), mul_sc_r(16n, al, bh))),
          Equal.trans(Nat, l4, l5, Nat.add(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh)))), cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(Nat.mul(sa, bl), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), cong_l(Nat.mul(sa, bl), WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), mul_sc_l(16n, ah, bl))),
            cong_r(Nat.add(Nat.mul(al, bl), WD.sc(16n, Nat.mul(al, bh))), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb)), Nat.add(WD.sc(16n, Nat.mul(ah, bl)), WD.sc(32n, Nat.mul(ah, bh))), cong_r(WD.sc(16n, Nat.mul(ah, bl)), Nat.mul(sa, sb), WD.sc(32n, Nat.mul(ah, bh)), e6)))))))

Uses (13):
  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=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  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/w64mul.bend&name=cong_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=cong_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=cong_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=mul_sc_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=mul_sc_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend&name=sc_sc