def shift_lt_succ

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

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

74# 2^j < 2^(1 + j), and 2^j < 2^k for j < k (k = d + 1 + j)
75def shift_lt_succ(+one: Nat, +h1: {one == 1n : Nat}, +j: Nat) -> {Nat.is_lt(C.shift(j, one), C.shift(1n+j, one)) == True{} : Bool}:
76  %Equal.sym(Nat, Nat.double(C.shift(j, one)), Nat.add(C.shift(j, one), C.shift(j, one)), NA.double_self(C.shift(j, one))) : {Nat.is_lt(C.shift(j, one), _) == True{} : Bool}
77  I.lt_add_pos(C.shift(j, one), C.shift(j, one), shift_pos(one, h1, j))