theorem div_neg_iff_neg (a b : ℝ) (h : 0 < b) : a / b < 0 ↔ a < 0

theorem mul_lt_mul_iff_div_lt_div {a b c d : ℝ} (ha : a > 0) (hc : c > 0) : a * b < c * d ↔ b / c < d / a

theorem mul_lt_iff_lt_div (a b c : ℝ) (hb : 0 < b) : a * b < c ↔ a < c / b

theorem sqrt_mul_lt_sqrt {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) : √a * b < √c ↔ a * b ^ 2 < c

theorem sqrt_lt_sqrt_mul {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : √a < √c * b ↔ a < c * b ^ 2