def ne_high

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

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

196def ne_high(+x: Nat, +c: Nat, +y: Nat, h: {Nat.is_lt(x, c) == True{} : Bool}) -> {False{} == Nat.is_eq(Nat.add(c, y), x) : Bool}:
197  match x:
198    case 0n:
199      match c:
200        case 0n:
201          Empty.absurd({False{} == Nat.is_eq(y, 0n) : Bool}, Arith.clash(h))
202        case 1n+q:
203          {==}
204    case 1n+p:
205      match c:
206        case 0n:
207          Empty.absurd({False{} == Nat.is_eq(y, 1n+p) : Bool}, Arith.clash(h))
208        case 1n+q:
209          ne_high(p, q, y, h)