F64sqk.usq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend as F64sqk
Lines 25-27 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqk.bend&start_line=25&end_line=27

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqa.bend as AQ

# (s 2^32)^2 + r 2^64 == n 2^64 for s^2 + r == n
def usq(+s: Nat, +r: Nat, +n: Nat, +hn: {Nat.add(Nat.mul(s, s), r) == n : Nat}) -> {Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, r))) == C.shift(32n, C.shift(32n, n)) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, r))), Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), C.shift(32n, C.shift(32n, n)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.shift(32n, r))), Nat.mul(C.shift(32n, s), C.shift(32n, s)), C.shift(32n, C.shift(32n, Nat.mul(s, s))), AQ.sh_sq(32n, s)), Equal.trans(Nat, Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), C.shift(32n, C.shift(32n, n)), Equal.sym(Nat, C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), Nat.add(C.shift(32n, C.shift(32n, Nat.mul(s, s))), C.shift(32n, C.shift(32n, r))), WW.shift_add(32n, C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), Equal.trans(Nat, C.shift(32n, Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r))), C.shift(32n, C.shift(32n, Nat.add(Nat.mul(s, s), r))), C.shift(32n, C.shift(32n, n)), Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r)), C.shift(32n, Nat.add(Nat.mul(s, s), r)), Equal.sym(Nat, C.shift(32n, Nat.add(Nat.mul(s, s), r)), Nat.add(C.shift(32n, Nat.mul(s, s)), C.shift(32n, r)), WW.shift_add(32n, Nat.mul(s, s), r))), Equal.cong(Nat, Nat, z => C.shift(32n, C.shift(32n, z)), Nat.add(Nat.mul(s, s), r), n, hn))))

Uses (9):
  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.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/math/typed/f64sqa.bend&name=sh_sq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift