Nat.succ_pos: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/nat.bend as Nat
Lines 2535-2538 of bend-mathlib@0.8.1.0/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/nat.bend&start_line=2535&end_line=2538

import Base

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

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt