~/jendhub

law succ_lt_succ

bend-mathlib@0.8.1.0 · nat.bend:2552

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

2552# The successor preserves the strict order: a < b implies a + 1 < b + 1.
2553law succ_lt_succ:
2554  for -a: Nat
2555  for -b: Nat
2556  for h: lt(a, b)
2557  lt(1n+a, 1n+b)

Uses (2)

Used by (0)

No other definition uses this definition.