def lt_le_trans

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:154

import Base

154def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
155  succ_le_lt(a, c, le_trans(1n+a, b, c, lt_succ_le_succ(a, b, ab), bc))