def shk

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/lits.bend:13

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/crypto/secp256k1/consts.bend as K

13def shk(+k: Nat, +one: Nat, +v: Nat, +hv: {C.shift(k, one) == v : Nat}) -> {C.shift(1n+k, one) == Nat.add(v, v) : Nat}:
14  %Equal.sym(Nat, C.shift(1n+k, one), Nat.add(C.shift(k, one), C.shift(k, one)), Equal.sym(Nat, Nat.add(C.shift(k, one), C.shift(k, one)), C.shift(1n+k, one), K.shift_twice(k, one))) : {_ == Nat.add(v, v) : Nat}
15  %Equal.sym(Nat, C.shift(k, one), v, hv) : {Nat.add(_, C.shift(k, one)) == Nat.add(v, v) : Nat}
16  %Equal.sym(Nat, C.shift(k, one), v, hv) : {Nat.add(v, _) == Nat.add(v, v) : Nat}
17  {==}