Limbs.sc_lt_succ: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
Lines 148-154 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&start_line=148&end_line=154

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

# 2^k < 2^(k+1)
def 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}:
  +x = WD.sc(k, one)
  +a = N.lt_add_left(0n, x, x, sc_pos1(k, one, h1))
  %N.add_zero(x) : {Nat.is_lt(_, WD.sc(1n+k, one)) == True{} : Bool}
  %M.sc_dbl(k, one) : {Nat.is_lt(Nat.add(x, 0n), _) == True{} : Bool}
  a

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=sc_pos1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc