law le_add_left
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2258# Adding on the left never decreases a natural: n <= m + n.
2259law le_add_left:
2260 for n: Nat
2261 for m: Nat
2262 le(n, Nat.add(m, n))
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2258# Adding on the left never decreases a natural: n <= m + n.
2259law le_add_left:
2260 for n: Nat
2261 for m: Nat
2262 le(n, Nat.add(m, n))