def qs_fin2

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

155def qs_fin2(+x: Nat, +r: Nat, +B: Nat, +bp: Nat, +hB: {B == 1n+bp : Nat}, p: {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> {Nat.div(x, 1n+bp) == r : Nat} & {Nat.mod(x, 1n+bp) == Nat.sub(x, Nat.mul(r, 1n+bp)) : Nat}:
156  (+a, +c) = p
157  div_uniq(x, r, bp, L.subst(Nat, z => {Nat.is_le(Nat.mul(r, z), x) == True{} : Bool}, B, 1n+bp, hB, a), L.subst(Nat, z => {Nat.is_lt(x, Nat.mul(1n+r, z)) == True{} : Bool}, B, 1n+bp, hB, c))