theorem div_add_div_comm_fact_denum {a b c d : ℝ} (hd : d ≠ 0) : a / b + c / (b * d) = (a * d + c) / (b * d)

theorem div_sub_div_comm_fact_denum {a b c d : ℝ} (hd : d ≠ 0) : a / b - c / (b * d) = (a * d - c) / (b * d)

theorem min_div_mul_div_simp_comm_fact {a b c d e : ℝ} (hc : c ≠ 0) : -(a / (b * c)) * (d * c / e) = -(a * d / (b * e))

theorem mul_div_cancel_den {a b c : ℝ} (ha : a ≠ 0) : a * (b / (a * c)) = b / c

theorem div_gt_self {a b : ℝ} (ha : a > 0) (hb : b > 0) (hb' : b < 1) : a / b > a

theorem mul_eq_iff_eq_div {a b c : ℝ} (ha : a ≠ 0) : a * b = c ↔ b = c / a