law pow_lt_pow_left

bend-mathlib@0.8.1.0 · nat.bend:3389

import Base

3389# Positive powers are strictly monotone in the base: a < b implies a^(1 + n) < b^(1 + n).
3390law pow_lt_pow_left:
3391  for a: Nat
3392  for b: Nat
3393  for h: lt(a, b)
3394  for n: Nat
3395  lt(Nat.pow(a, 1n+n), Nat.pow(b, 1n+n))