law one_le_pow
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2232# A power of a positive base is at least one: 1 <= (1 + a)^n.
2233law one_le_pow:
2234 for n: Nat
2235 for a: Nat
2236 le(1n, Nat.pow(1n+a, n))
import bend-mathlib@0.8.1.0/nat.bend as Natimport Base
2232# A power of a positive base is at least one: 1 <= (1 + a)^n.
2233law one_le_pow:
2234 for n: Nat
2235 for a: Nat
2236 le(1n, Nat.pow(1n+a, n))