def pick_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:150

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

150def pick_zero(+x: Nat, +y: Nat) -> {L.pick1(0n, x, y) == y : Nat}:
151  %Equal.sym(Nat, Nat.mul(x, 0n), 0n, NA.mul_zero(x)) : {Nat.add(_, Nat.mul(y, 1n)) == y : Nat}
152  %Equal.sym(Nat, Nat.mul(y, 1n), y, NA.mul_one(y)) : {Nat.add(0n, _) == y : Nat}
153  %Equal.sym(Nat, Nat.add(0n, y), y, SR.zero_add(y)) : {_ == y : Nat}
154  {==}