def small_ev

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:203

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

203def small_ev(+k: Nat) -> {LV.ev([k]) == k : Nat}:
204  %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(k, _) == k : Nat}
205  %Equal.sym(Nat, Nat.add(k, 0n), k, NA.add_zero(k)) : {_ == k : Nat}
206  {==}