apply Nat.le_sub_of_add_le
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a ≤ (x + 1 + 1) ^ (a + b) - (x + 1 + 1) ^ a
case h
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + 1) ^ a ≤ (x + 1 + 1) ^ (a + b)