apply Nat.pow_le_pow_left (Nat.le_succ _)
a b x : ℕ
⊢ (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

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

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

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