~/jendhub

def u.le_trans

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

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
import Base

385# a <= b <= c
386def u.le_trans(+a: U32, +b: U32, +c: U32, +h1: {ule(a, b) == True{} : Bool}, +h2: {ule(b, c) == True{} : Bool}) -> {ule(a, c) == True{} : Bool}:
387  u.le_le.go(U32.cmp(a, b), a, b, c, {==}, h1, h2)

Uses (5)

Used by (1)