def up_okg

import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt

import Base

102def up_okg(+x: U32, +r: U32, +m: U32) -> Bool:
103  Bool.and(U32.is_lt(r, m), U32.is_le(U32.mul(U32.add(r, 1), U32.add(r, 1)), x))

Uses (7)