apply (Nat.exists_eq_add_of_le hab).elim
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), b = a + a_1 → y ^ a - x ^ a ≤ y ^ b - x ^ b