def lt_asym

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:202

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

202def lt_asym(+a: Nat, +b: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, ba: {Nat.is_lt(b, a) == True{} : Bool}) -> Empty:
203  L.true_not_false(Nat.is_lt(a, a), lt_trans(a, b, a, ab, ba), lt_irrefl(a))