def qs_fin

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64dm.bend:151

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU

151def qs_fin(+x: Nat, +r: Nat, +bp: Nat, +hB: {SW.value(WU.U64{0, 0}) == 0n : Nat}, p: {Nat.is_le(Nat.mul(r, 1n+bp), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, 1n+bp)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
152  (+a, +c) = p
153  div_uniq(x, r, bp, a, c)