def sc_add2

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64mul.bend:121

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A

121def sc_add2(+k: Nat, +x: Nat, +y: Nat) -> {WD.sc(k, Nat.add(x, y)) == Nat.add(WD.sc(k, x), WD.sc(k, y)) : Nat}:
122  Equal.sym(Nat, Nat.add(WD.sc(k, x), WD.sc(k, y)), WD.sc(k, Nat.add(x, y)), A.sc_add(k, x, y))