rw [div_eq_mul_inv, Real.rpow_neg hx, Real.rpow_neg hy, Real.div_rpow hy hx]
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ (-s) / y ^ (-s) = (y / x) ^ s
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x ^ s)⁻¹ * (y ^ s)⁻¹⁻¹ = y ^ s / x ^ s