def lt_trans

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

import Base

160def lt_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_lt(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
161  lt_le_trans(a, b, c, ab, lt_le(b, c, bc))