theorem Real.mul_mul_comm_last_second (a b c : ℝ) : a * b * c = a * c * b