def isqrt_char

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:55

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

55def isqrt_char(+n: Nat, +s: Nat, +h1: {Nat.is_le(Nat.mul(s, s), n) == True{} : Bool}, +h2: {Nat.is_lt(n, Nat.mul(1n+s, 1n+s)) == True{} : Bool}) -> {M.isqrt(n) == s : Nat}:
56  N.le_antisym(M.isqrt(n), s, N.lt_succ_le(M.isqrt(n), s, isqrt_lt(n, 1n+s, h2)), isqrt_ge(n, s, h1))