def lt_le_trans

bendtorch-core@0.1.0.0 · src/storage/arith.bend:257

import Base

257def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool},
258  bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
259  match a:
260    case 0n:
261      match b:
262        case 0n:
263          Empty.absurd({Nat.is_lt(0n, c) == True{} : Bool}, clash(ab))
264        case 1n+q:
265          match c:
266            case 0n:
267              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(bc))
268            case 1n+r:
269              {==}
270    case 1n+p:
271      match b:
272        case 0n:
273          Empty.absurd({Nat.is_lt(1n+p, c) == True{} : Bool}, clash(ab))
274        case 1n+q:
275          match c:
276            case 0n:
277              Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(bc))
278            case 1n+r:
279              lt_le_trans(p, q, r, ab, bc)