def u.le_lt.go

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:347

import Base

347def u.le_lt.go(c1: Cmp, +a: U32, +b: U32, +c: U32, +e1: {U32.cmp(a, b) == c1 : Cmp}, +h1: {Cmp.is_le(c1) == True{} : Bool}, +h2: {U32.cmp(b, c) == LT{} : Cmp}) -> {U32.cmp(a, c) == LT{} : Cmp}:
348  match c1:
349    case LT{}:
350      u.cmp_lt_trans(a, b, c, e1, h2)
351    case EQ{}:
352      %Equal.sym(U32, a, b, u.eq(a, b, e1)) : {U32.cmp(_, c) == LT{} : Cmp}
353      h2
354    case GT{}:
355      Empty.absurd({U32.cmp(a, c) == LT{} : Cmp}, ab.ft(h1))