def lt_succ

bendtorch-core@0.1.0.0 · src/storage/arith.bend:281

import Base

281def lt_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(a, 1n+b) == True{} : Bool}:
282  match a:
283    case 0n:
284      {==}
285    case 1n+p:
286      match b:
287        case 0n:
288          Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, clash(h))
289        case 1n+q:
290          lt_succ(p, q, h)