law succ_le_succ
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1418# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1419law succ_le_succ:
1420 for -a: Nat
1421 for -b: Nat
1422 for h: le(a, b)
1423 le(1n+a, 1n+b)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1418# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1419law succ_le_succ:
1420 for -a: Nat
1421 for -b: Nat
1422 for h: le(a, b)
1423 le(1n+a, 1n+b)