law le_of_lt_succ
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2572# Below a successor is at most: m < n + 1 implies m <= n.
2573law le_of_lt_succ:
2574 for m: Nat
2575 for n: Nat
2576 for h: lt(m, 1n+n)
2577 le(m, n)
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2572# Below a successor is at most: m < n + 1 implies m <= n.
2573law le_of_lt_succ:
2574 for m: Nat
2575 for n: Nat
2576 for h: lt(m, 1n+n)
2577 le(m, n)