law add_ev
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:63
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as Value
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/src/crypto/poly1305/limbs.bend as Li
63law add_ev:
64 for +a: List<&2, U32>
65 for +b: List<&2, U32>
66 for +b1: Nat
67 for +b2: Nat
68 for +ha: {le_all(a, b1) == True{} : Bool}
69 for +hb: {le_all(b, b2) == True{} : Bool}
70 for +hf: {C.fits(32n, Nat.add(b1, b2)) == True{} : Bool}
71 {ev(Li.add(a, b)) == Nat.add(ev(a), ev(b)) : Nat}