def le_dd

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

import Base

157def le_dd(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
158  match u v:
159    case 0n 0n:
160      {==}
161    case 0n 1n+q:
162      {==}
163    case 1n+p 0n:
164      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
165    case 1n+p 1n+q:
166      le_dd(p, q, h)