def nat_nonzero

stelliferous@0.0.2.0 · proofs/u32_division.bend:138

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

138def nat_nonzero(+b: Nat,h: {Nat.is_lt(0n,b) == True{} : Bool}) -> {Nat.is_eq(b,0n) == False{} : Bool}:
139  match b:
140    case 0n:
141      Empty.absurd({Nat.is_eq(0n,0n) == False{} : Bool},WordEncoding.false_true(h))
142    case 1n+p:
143      {==}