apply Nat.add_le_of_le_sub _ blah5
case h
a b y x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + y) ^ a ≤ (x + 1 + y) ^ (a + b)

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

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

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

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