def bq.le_trans

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:179

import Base

179def bq.le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
180  match a b c:
181    case 0n _ _:
182      bq.le_zero(c)
183    case 1n+ap 0n _:
184      Empty.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, bq.ft(e))
185    case 1n+ap 1n+bp 0n:
186      Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, bq.ft(f))
187    case 1n+ap 1n+bp 1n+cp:
188      bq.le_trans(ap, bp, cp, e, f)