~/jendhub

def divmod_eq

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

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

16def divmod_eq(+a: Nat, +bp: Nat) -> {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}:
17  R.dm_eq(bp, a)

Uses (6)

Used by (1)