def bq.le_antisym

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

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U

205def bq.le_antisym(x: Nat, y: Nat, h1: {Nat.is_le(x, y) == True{} : Bool}, h2: {Nat.is_le(y, x) == True{} : Bool}) -> {x == y : Nat}:
206  match x y:
207    case 0n 0n:
208      {==}
209    case 0n 1n+yp:
210      Empty.absurd({0n == 1n+yp : Nat}, bq.ft(h2))
211    case 1n+xp 0n:
212      Empty.absurd({1n+xp == 0n : Nat}, bq.ft(h1))
213    case 1n+xp 1n+yp:
214      U.uq.succ_cong(xp, yp, bq.le_antisym(xp, yp, h1, h2))