convert div_rpow_neg_eq_rpow_div (s := -s) hx hy using 1
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = (y / x) ^ (-s)
case h.e'_2
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = x ^ (- -s) / y ^ (- -s)