def DivMod.euclid

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

import Base

277def DivMod.euclid(+a: Nat, +bp: Nat) -> Type:
278  {a == Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) : Nat}