def AP.double_zero

bend-osdev-array@0.1.0.1 · PROOF.bend:107

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

107def AP.double_zero(x: Nat, e: {Nat.double(x) == 0n : Nat}) -> {x == 0n : Nat}:
108  match x:
109    case 0n:
110      {==}
111    case 1n+p:
112      Empty.absurd({1n+p == 0n : Nat}, AP.sz(1n+Nat.double(p), e))

Uses (4)

Used by (2)