Theorem: Real.div_pow_eq_mul_pow_neg (CvxLean/Lib/Math/Data/Real.lean)

State before:
a b c : ℝ
hb : 0 ≤ b
⊢ a / b ^ c = a * b ^ (-c)
Tactic:
rw [div_eq_mul_inv, ← rpow_neg hb]
State after:
no goals