def sc_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:303

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

303def sc_pos(+k: Nat) -> {Nat.is_lt(0n, sc(k, 1n)) == True{} : Bool}:
304  match k:
305    case 0n:
306      {==}
307    case 1n+j:
308      N.double_lt(0n, sc(j, 1n), sc_pos(j))