Theorem: div_rpow_eq_rpow_div_neg (PrimeNumberTheoremAnd/ZetaBounds.lean)

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

State before:
case h.e'_2
x y s : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ s / y ^ s = x ^ (- -s) / y ^ (- -s)
Tactic:
simp only [neg_neg]
State after:
no goals