def ud.nz

bend-osdev-u32@0.1.0.0 · PROOF.bend:1801

import Base

1801def ud.nz(x: Nat, e: {Nat.is_eq(x, 0n) == False{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}:
1802  match x:
1803    case 0n:
1804      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, un.tf(e))
1805    case 1n+ +p:
1806      {==}