def lt_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bounds.bend:16

import Base

16def lt_one(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(0n, one) == True{} : Bool}:
17  %Equal.sym(Nat, one, 1n, h1) : {Nat.is_lt(0n, _) == True{} : Bool}
18  {==}