def ne_low

bendtorch-core@0.1.0.0 · src/storage/api.bend:181

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

181def ne_low(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(x, Nat.add(c, y)) : Bool}:
182  match x:
183    case 0n:
184      match c:
185        case 0n:
186          Empty.absurd({False{} == Nat.is_eq(0n, y) : Bool}, Arith.clash(h))
187        case 1n+q:
188          {==}
189    case 1n+p:
190      match c:
191        case 0n:
192          Empty.absurd({False{} == Nat.is_eq(1n+p, y) : Bool}, Arith.clash(h))
193        case 1n+q:
194          ne_low(p, q, y, h)