def un.dz0

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

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

2063def un.dz0(v: Nat, e: {Nat.double(v) == 0n : Nat}) -> {v == 0n : Nat}:
2064  match v:
2065    case 0n:
2066      {==}
2067    case 1n+ +p:
2068      Empty.absurd({1n+p == 0n : Nat}, un.sz(1n+Nat.double(p), e))

Uses (4)

Used by (2)