law lt_succ_self
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1406# Every natural is less than its successor: n < n + 1.
1407law lt_succ_self:
1408 for n: Nat
1409 lt(n, 1n+n)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
1406# Every natural is less than its successor: n < n + 1.
1407law lt_succ_self:
1408 for n: Nat
1409 lt(n, 1n+n)