F64sqv.psq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend as F64sqv
Lines 35-37 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqv.bend&start_line=35&end_line=37

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

# (2^k)^2 as one shift
def psq(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat) -> {Nat.mul(C.shift(k, one), C.shift(k, one)) == C.shift(Nat.add(k, k), one) : Nat}:
  Equal.trans(Nat, Nat.mul(C.shift(k, one), C.shift(k, one)), C.shift(k, C.shift(k, Nat.mul(one, one))), C.shift(Nat.add(k, k), one), AQ.sh_sq(k, one), Equal.trans(Nat, C.shift(k, C.shift(k, Nat.mul(one, one))), C.shift(k, C.shift(k, one)), C.shift(Nat.add(k, k), one), Equal.cong(Nat, Nat, z => C.shift(k, C.shift(k, z)), Nat.mul(one, one), one, mone(one, h1)), Equal.sym(Nat, C.shift(Nat.add(k, k), one), C.shift(k, C.shift(k, one)), WW.shift_comp(k, k, one))))

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