def shift_le_k

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

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/ineq.bend as I

36def shift_le_k(+j: Nat, +k: Nat, +x: Nat, +d: Nat, +hd: {Nat.add(d, j) == k : Nat}) -> {Nat.is_le(C.shift(j, x), C.shift(k, x)) == True{} : Bool}:
37  I.le_subst_r(C.shift(j, x), C.shift(Nat.add(d, j), x), C.shift(k, x), Equal.cong(Nat, Nat, z => C.shift(z, x), Nat.add(d, j), k, hd), shift_more(d, j, x))