~/jendhub

def le_ds

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

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

179def le_ds(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), 1n+Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
180  match u v:
181    case 0n v:
182      le_zero(v)
183    case 1n+p 0n:
184      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
185    case 1n+p 1n+q:
186      le_ds(p, q, h)

Uses (7)

Used by (1)