def cadd

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM

21# a + b == a' + b'
22def cadd(+a: Nat, +a2: Nat, +b: Nat, +b2: Nat, +ea: {a == a2 : Nat}, +eb: {b == b2 : Nat}) -> {Nat.add(a, b) == Nat.add(a2, b2) : Nat}:
23  tr(Nat.add(a, b), Nat.add(a2, b), Nat.add(a2, b2), WM.cong_l(a, a2, b, ea), WM.cong_r(a2, b, b2, eb))