def DivMod.rem_lt

bend-collections-laws-crypto@1.0.0.0 · spec/math/natural.bend:280

import Base

280def DivMod.rem_lt(+a: Nat, +bp: Nat) -> Type:
281  {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}