~/jendhub

law pos_of_ne_zero

bend-mathlib@0.8.1.0 · nat.bend:2657

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

2657# A natural that does not test equal to zero is positive.
2658law pos_of_ne_zero:
2659  for n: Nat
2660  for h: {Nat.is_eq(n, 0n) == False{} : Bool}
2661  lt(0n, n)

Uses (6)

Used by (1)