def ns.eq_zero

bend-osdev-word64@0.1.1.0 · proof_shift.bend:95

import Base
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

95def ns.eq_zero(x: Nat, e: {Nat.is_eq(x, 0n) == True{} : Bool}) -> {x == 0n : Nat}:
96  match x:
97    case 0n:
98      {==}
99    case 1n+ +p:
100      Empty.absurd({1n+p == 0n : Nat}, P.wn.ft(e))