def bq.lt_le

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

import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch

import Base

170def bq.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
171  match x y:
172    case 0n _:
173      bq.le_zero(y)
174    case 1n+xp 0n:
175      Empty.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, bq.ft(h))
176    case 1n+xp 1n+yp:
177      bq.lt_le(xp, yp, h)

Uses (7)

Used by (2)