def lt_dd

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

import Base

292def lt_dd(+x: Nat, +c: Nat, h: {Nat.is_lt(Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
293  match x c:
294    case 0n 0n:
295      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
296    case 0n 1n+q:
297      {==}
298    case 1n+p 0n:
299      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
300    case 1n+p 1n+q:
301      lt_dd(p, q, h)