def cmp_lt
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmpimport Base
73def cmp_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.cmp(a, b) == LT{} : Cmp}:
74 lt_c(Nat.cmp(a, b), h)
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmpimport Base
73def cmp_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.cmp(a, b) == LT{} : Cmp}:
74 lt_c(Nat.cmp(a, b), h)