theorem Real.inv_rpow_logb {b : ℝ} (hb : 0 < b) (hb' : b ≠ 1) {x : ℝ} (hx : 0 < x) : b⁻¹ ^ logb b x = x⁻¹