def fits_add_l

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:66

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

66# x <= y + z and fits(k, y + z)
67def fits_add_l(+k: Nat, +y: Nat, +z: Nat, +h: {C.fits(k, Nat.add(y, z)) == True{} : Bool}) -> {C.fits(k, y) == True{} : Bool}:
68  fits_le(k, y, Nat.add(y, z), N.le_add_right(y, z), h)