def lt_of_cmp

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:96

import Base

96def lt_of_cmp(+a: Nat, +b: Nat, +h: {Nat.cmp(a, b) == LT{} : Cmp}) -> {Nat.is_lt(a, b) == True{} : Bool}:
97  Equal.cong(Cmp, Bool, t => Cmp.is_lt(t), Nat.cmp(a, b), LT{}, h)