def bq.not_lt

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

import Base

216def bq.not_lt(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
217  match x y:
218    case 0n 0n:
219      {==}
220    case 0n 1n+yp:
221      Empty.absurd({Nat.is_le(1n+yp, 0n) == True{} : Bool}, bq.tf(e))
222    case 1n+xp 0n:
223      {==}
224    case 1n+xp 1n+yp:
225      bq.not_lt(xp, yp, e)