law pow_lt_pow_right

bend-mathlib@0.8.1.0 · nat.bend:3367

import Base

3367# Powers of a base above one are strictly monotone in the exponent: i < j implies (2 + a)^i < (2 + a)^j.
3368law pow_lt_pow_right:
3369  for a: Nat
3370  for i: Nat
3371  for j: Nat
3372  for h: lt(i, j)
3373  lt(Nat.pow(2n+a, i), Nat.pow(2n+a, j))