rw [← Nat.sub_add_comm]
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1) + x ^ a
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) + x ^ a - x ^ (a + 1)

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)