def fits_add_r

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

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

70def fits_add_r(+k: Nat, +y: Nat, +z: Nat, +h: {C.fits(k, Nat.add(y, z)) == True{} : Bool}) -> {C.fits(k, z) == True{} : Bool}:
71  fits_le(k, z, Nat.add(y, z), le_add_l(y, z), h)