def cmp_lt

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmp

import 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)

Uses (6)