def lt_trans

bend-kit-collections@0.1.4.1 · PROOF.bend:233

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF

import Base

233def lt_trans(
234  ~K: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), +x: K, +y: K, +z: K,
235  e1: {Cmp.is_lt(cmp(x, y)) == True{} : Bool},
236  e2: {Cmp.is_lt(cmp(y, z)) == True{} : Bool}
237) -> {Cmp.is_lt(cmp(x, z)) == True{} : Bool}:
238  lt_true(cmp(x, z), trans(x, y, z, lt_of(cmp(x, y), e1), lt_of(cmp(y, z), e2)))

Uses (6)

Used by (2)