def nlt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fwrap.bend:100

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

100# not (x < m + 1) is m < x
101def nlt(x: Nat, m: Nat) -> {Bool.not(Nat.is_lt(x, 1n+m)) == Nat.is_lt(m, x) : Bool}:
102  match x m:
103    case 0n _:
104      Equal.sym(Bool, Nat.is_lt(m, 0n), False{}, N.not_lt_zero(m))
105    case 1n+y 0n:
106      %Equal.sym(Bool, Nat.is_lt(y, 0n), False{}, N.not_lt_zero(y)) : {Bool.not(_) == True{} : Bool}
107      {==}
108    case 1n+y 1n+k:
109      nlt(y, k)