def shift_more

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:28

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/nat.bend as N

28# 2^k x <= 2^(d + k) x
29def shift_more(d: Nat, +k: Nat, +x: Nat) -> {Nat.is_le(C.shift(k, x), C.shift(Nat.add(d, k), x)) == True{} : Bool}:
30  match d:
31    case 0n:
32      N.le_refl(C.shift(k, x))
33    case 1n+ +e:
34      N.le_trans(C.shift(k, x), C.shift(Nat.add(e, k), x), Nat.double(C.shift(Nat.add(e, k), x)), shift_more(e, k, x), N.double_self_le(C.shift(Nat.add(e, k), x)))