rw [Nat.pow_succ, Nat.pow_succ]
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ (x + 1) < z ^ (y + 1)
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x * z < z ^ y * z