~/jendhub

law pow_pos

bend-mathlib@0.8.1.0 · nat.bend:2246

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

2246# A power of a positive base is positive: 0 < (1 + a)^n.
2247law pow_pos:
2248  for n: Nat
2249  for a: Nat
2250  lt(0n, Nat.pow(1n+a, n))

Uses (9)

Used by (1)