def qle_fin

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

import Base

159def qle_fin(+x: Nat, +r: Nat, +B: Nat, p: {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool} & {Nat.is_lt(x, Nat.mul(1n+r, B)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(r, B), x) == True{} : Bool}:
160  (+a, +c) = p
161  a