def le_sd

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

import Base

168def le_sd(+u: Nat, +v: Nat, h: {Nat.is_le(1n+Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(1n+u, v) == True{} : Bool}:
169  match u v:
170    case 0n 0n:
171      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, clash(h))
172    case 0n 1n+q:
173      le_zero(q)
174    case 1n+p 0n:
175      Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, clash(h))
176    case 1n+p 1n+q:
177      le_sd(p, q, h)