rw [Nat.pow_succ]
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ y * (x + 1)