def pos_nat

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:170

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

170def pos_nat(+x: Nat, +h: {Cmp.is_eq(Nat.cmp(x, 0n)) == False{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}:
171  match x:
172    case 0n:
173      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(h))
174    case 1n+k:
175      {==}