~/jendhub

def uq.lt_succ_r

bend-osdev-algo@0.1.0.0 · proof_u32.bend:161

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

161def uq.lt_succ_r(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
162  match x y:
163    case 0n _:
164      {==}
165    case 1n+xp 0n:
166      Empty.absurd({Nat.is_lt(1n+xp, 1n) == True{} : Bool}, uq.ft(h))
167    case 1n+xp 1n+yp:
168      uq.lt_succ_r(xp, yp, h)

Uses (5)

Used by (1)