law pow_le_pow_right

bend-mathlib@0.8.1.0 · nat.bend:3342

import Base

3342# Powers of a positive base are monotone in the exponent: i <= j implies (1 + a)^i <= (1 + a)^j.
3343law pow_le_pow_right:
3344  for a: Nat
3345  for i: Nat
3346  for j: Nat
3347  for h: le(i, j)
3348  le(Nat.pow(1n+a, i), Nat.pow(1n+a, j))