def gt.lt_succ_r

bend-osdev-gf@0.1.1.0 · proof_tab.bend:124

import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab

import Base

124def gt.lt_succ_r(+x: Nat, +y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_lt(x, 1n+y) == True{} : Bool}:
125  match x y:
126    case 0n _:
127      {==}
128    case 1n+p 0n:
129      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, gt.ft(h))
130    case 1n+p 1n+q:
131      gt.lt_succ_r(p, q, h)

Uses (5)

Used by (2)