theorem mul_mul_comm_last_first (a b c : ℝ>0) : a * b * c = c * b * a

theorem mul_mul_comm_last_second (a b c : ℝ>0) : a * b * c = a * c * b

theorem mul_mul_mul_comm_last_first (a b c d : ℝ>0) : a * b * c * d = d * b * c * a

theorem mul_mul_mul_comm_third_first (a b c d : ℝ>0) : a * b * c * d = c * b * a * d

theorem mul_mul_mul_comm_third_second (a b c d : ℝ>0) : a * b * c * d = a * c * b * d

theorem PReal.mul_inv_cancel (a : ℝ>0) : a * a⁻¹ = 1

theorem PReal.mul_lt_mul_right (a b c : ℝ>0) : b * a < c * a ↔ b < c