apply Nat.le_sub_of_add_le
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)
case h.h
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a

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