def leb_trans

bend-ml-llama@0.2.1.0 · main.bend:536

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

536# a <= b  and  b <= c  ->  a <= c
537def leb_trans(a: Nat, b: Nat, c: Nat, e1: {True{} == TA.leb(a, b) : Bool}, e2: {True{} == TA.leb(b, c) : Bool}) -> {True{} == TA.leb(a, c) : Bool}:
538  match a b c:
539    case 0n _ _:
540      {==}
541    case 1n+p 0n _:
542      %e1 : TA.BD(_, Unit, {True{} == TA.leb(1n+p, c) : Bool})
543      Unit{}
544    case 1n+p 1n+q 0n:
545      %e2 : TA.BD(_, Unit, {True{} == TA.leb(1n+p, 0n) : Bool})
546      Unit{}
547    case 1n+p 1n+q 1n+r:
548      leb_trans(p, q, r, e1, e2)