def DN

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

72def DN(+one: Nat, +x: U32, +r: U32) -> Type:
73  {Nat.is_le(sq(v(r)), v(x)) == True{} : Bool} & {Nat.is_lt(v(r), WD.sc(16n, one)) == True{} : Bool}