~/jendhub

law succ_pos

bend-mathlib@0.8.1.0 · nat.bend:2535

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

2535# Every successor is positive: 0 < n + 1.
2536law succ_pos:
2537  for -n: Nat
2538  lt(0n, 1n+n)

Uses (2)

Used by (0)

No other definition uses this definition.