CMB_eq_of_one_lt_q

public lemma CMB_eq_of_one_lt_q {b q : ℝ≥0} (hq : 1 < q) :    CMB b q = 2 * (q / (q - 1) * b ^ 2) ^ (q : ℝ)⁻¹ := by  suffices ENNReal.toNNReal 2 * q ^ (q : ℝ)⁻¹ *      (ENNReal.ofReal |q - 1|⁻¹).toNNReal ^ (q : ℝ)⁻¹ *      (b ^ 2) ^ (q : ℝ)⁻¹ = 2 * (q / (q - 1) * b ^ 2) ^ (q : ℝ)⁻¹ by    simpa [CMB, C_realInterpolation, C_realInterpolation_ENNReal]  norm_cast  have e₁ : (ENNReal.ofReal |q - 1|⁻¹).toNNReal = (q - 1)⁻¹ := by    rw [ofReal_inv_of_pos]; swap    · rw [abs_sub_pos, NNReal.coe_ne_one]; exact hq.ne'    rw [toNNReal_inv, inv_inj, ← NNReal.coe_one, ← NNReal.coe_sub hq.le, NNReal.abs_eq,      ofReal_coe_nnreal, toNNReal_coe]  rw [e₁, mul_assoc, ← NNReal.mul_rpow, mul_assoc, ← NNReal.mul_rpow, ← mul_assoc, div_eq_mul_inv]