def root_uniq

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

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

221def root_uniq(+r: Nat, +s: Nat, +n: Nat, +h1: {Nat.is_le(sq(r), n) == True{} : Bool}, +h2: {Nat.is_lt(n, sq(1n+r)) == True{} : Bool}, +h3: {Nat.is_le(sq(s), n) == True{} : Bool}, +h4: {Nat.is_lt(n, sq(1n+s)) == True{} : Bool}) -> {r == s : Nat}:
222  N.le_antisym(r, s, root_le(r, s, n, h1, h4, Nat.is_lt(s, r), {==}), root_le(s, r, n, h3, h2, Nat.is_lt(r, s), {==}))