Fwrap.nlt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as Fwrap
Lines 100-109 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&start_line=100&end_line=109

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

# not (x < m + 1) is m < x
def nlt(x: Nat, m: Nat) -> {Bool.not(Nat.is_lt(x, 1n+m)) == Nat.is_lt(m, x) : Bool}:
  match x m:
    case 0n _:
      Equal.sym(Bool, Nat.is_lt(m, 0n), False{}, N.not_lt_zero(m))
    case 1n+y 0n:
      %Equal.sym(Bool, Nat.is_lt(y, 0n), False{}, N.not_lt_zero(y)) : {Bool.not(_) == True{} : Bool}
      {==}
    case 1n+y 1n+k:
      nlt(y, k)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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/lib/nat.bend&name=not_lt_zero