def u.le_le.go

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

import Base

375def u.le_le.go(c1: Cmp, +a: U32, +b: U32, +c: U32, +e1: {U32.cmp(a, b) == c1 : Cmp}, +h1: {Cmp.is_le(c1) == True{} : Bool}, +h2: {ule(b, c) == True{} : Bool}) -> {ule(a, c) == True{} : Bool}:
376  match c1:
377    case LT{}:
378      u.le_of_lt(a, c, u.lt_le(a, b, c, cm.is_lt_of(U32.cmp(a, b), e1), h2))
379    case EQ{}:
380      %Equal.sym(U32, a, b, u.eq(a, b, e1)) : {Cmp.is_le(U32.cmp(_, c)) == True{} : Bool}
381      h2
382    case GT{}:
383      Empty.absurd({ule(a, c) == True{} : Bool}, ab.ft(h1))