def divmod_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/misc.bend:19

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

19def divmod_lt(+a: Nat, +bp: Nat) -> {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}:
20  R.dm_lt(bp, a)