def le_succ

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

import Base

434def le_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
435  match a:
436    case 0n:
437      {==}
438    case 1n+p:
439      match b:
440        case 0n:
441          Empty.absurd({Nat.is_le(1n+p, 1n) == True{} : Bool}, clash(h))
442        case 1n+q:
443          le_succ(p, q, h)