law le_succ
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
383# Every natural is at most its successor: n <= n + 1.
384law le_succ:
385 for n: Nat
386 le(n, 1n+n)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
383# Every natural is at most its successor: n <= n + 1.
384law le_succ:
385 for n: Nat
386 le(n, 1n+n)