def sq_exact
bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:63
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
63def sq_exact(+one: Nat, +h1: {one == 1n : Nat}, +r: U32, +hb: {Nat.is_lt(v(r), WD.sc(16n, one)) == True{} : Bool}) -> {v(U32.mul(r, r)) == sq(v(r)) : Nat}:
64 PD.mul32(one, h1, r, r, WM.prod_lt(one, h1, v(r), v(r), hb, hb))