law ne_zero_pos

lawful-words@0.1.0.0 · proof_u32.bend:831

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

831law ne_zero_pos:
832  for +y: Nat
833  for +h: {Nat.is_eq(y, 0n) == False{} : Bool}
834  {Nat.is_lt(0n, y) == True{} : Bool}

Uses (6)

Used by (2)