Value.add1: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as Value
Lines 59-61 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend&start_line=59&end_line=61

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/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A

# the exact U32 sum of two limbs whose bounds add up within 32 bits
def add1(+x: U32, +y: U32, +b1: Nat, +b2: Nat, +hx: {Nat.is_le(v(x), b1) == True{} : Bool}, +hy: {Nat.is_le(v(y), b2) == True{} : Bool}, +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
  WA.add_exact(1n, {==}, x, y, A.fits_le(32n, Nat.add(v(x), v(y)), Nat.add(b1, b2), A.le_add2(v(x), v(y), b1, b2, hx, hy), hf))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend&name=fits_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend&name=le_add2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=add_exact
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=fits