def main_fin

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:257

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

257def main_fin(+x: U32, +rd: U32, +m: U32, +fu: Nat, q: {Nat.is_le(sq(v(up32g(fu, x, rd, up_okg(x, rd, m), m))), v(x)) == True{} : Bool} & {Nat.is_lt(v(x), sq(1n+v(up32g(fu, x, rd, up_okg(x, rd, m), m)))) == True{} : Bool}) -> {v(up32g(fu, x, rd, up_okg(x, rd, m), m)) == M.isqrt(v(x)) : Nat}:
258  (h3, h4) = q
259  is_isqrt(v(up32g(fu, x, rd, up_okg(x, rd, m), m)), v(x), h3, h4)