apply Nat.succ_le_of_lt
case succ_succ.right.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 ≤ (x + 1) ^ y
case succ_succ.right.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < (x + 1) ^ y