~/jendhub

law lt_of_succ_lt_succ

bend-mathlib@0.8.1.0 · nat.bend:2562

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

2562# The strict order of successors is the strict order of the naturals: a + 1 < b + 1 implies a < b.
2563law lt_of_succ_lt_succ:
2564  for -a: Nat
2565  for -b: Nat
2566  for h: lt(1n+a, 1n+b)
2567  lt(a, b)

Uses (2)

Used by (0)

No other definition uses this definition.