def sc_lt_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:148

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

148# 2^k < 2^(k+1)
149def sc_lt_succ(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(WD.sc(k, one), WD.sc(1n+k, one)) == True{} : Bool}:
150  +x = WD.sc(k, one)
151  +a = N.lt_add_left(0n, x, x, sc_pos1(k, one, h1))
152  %N.add_zero(x) : {Nat.is_lt(_, WD.sc(1n+k, one)) == True{} : Bool}
153  %M.sc_dbl(k, one) : {Nat.is_lt(Nat.add(x, 0n), _) == True{} : Bool}
154  a