def bq.lt_le_trans

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

import Base

190def bq.lt_le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
191  match a b c:
192    case 0n 0n _:
193      Empty.absurd({Nat.is_lt(0n, c) == True{} : Bool}, bq.ft(e))
194    case 0n 1n+bp 0n:
195      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(f))
196    case 0n 1n+bp 1n+cp:
197      {==}
198    case 1n+ap 0n _:
199      Empty.absurd({Nat.is_lt(1n+ap, c) == True{} : Bool}, bq.ft(e))
200    case 1n+ap 1n+bp 0n:
201      Empty.absurd({Nat.is_lt(1n+ap, 0n) == True{} : Bool}, bq.ft(f))
202    case 1n+ap 1n+bp 1n+cp:
203      bq.lt_le_trans(ap, bp, cp, e, f)