def un.lt_succ_r

bend-osdev-u32@0.1.0.0 · PROOF.bend:171

import Base

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