def le_lt_trans

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

import Base

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