theorem PReal.div_common_fact_cancel (a b c : ℝ>0) : a * b / (a * c) = b / c

theorem PReal.div_add_factor_num_den (a b c : ℝ>0) : a / b = a * c / (b * c)

theorem PReal.div_add_div_same (a b c : ℝ>0) : a / c + b / c = (a + b) / c

theorem PReal.no_denum_add_div (a b c : ℝ>0) : a + b / c = (a * c + b) / c

theorem PReal.mul_div_mul_cancel (a b c : ℝ>0) : a * b / (a * c) = b / c