def lt_add_cancel

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

import Base

460def lt_add_cancel(+c: Nat, +j: Nat, +k: Nat, h: {Nat.is_lt(Nat.add(c, j), Nat.add(c, k)) == True{} : Bool}) ->
461  {Nat.is_lt(j, k) == True{} : Bool}:
462  match c:
463    case 0n:
464      h
465    case 1n+r:
466      lt_add_cancel(r, j, k, h)