def lt_sd

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

import Base

303def lt_sd(+x: Nat, +c: Nat, h: {Nat.is_lt(1n+Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
304  match x c:
305    case 0n 0n:
306      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
307    case 0n 1n+q:
308      {==}
309    case 1n+p 0n:
310      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
311    case 1n+p 1n+q:
312      lt_sd(p, q, h)