@[simp]

theorem PReal.lt_add_right (x y : ℝ>0) : x < x + y

@[simp]

theorem PReal.lt_add_left (x y : ℝ>0) : x < y + x

@[simp]

theorem PReal.lt_add_iff_lt_cancel (x y z : ℝ>0) : x + z < x + y ↔ z < y

theorem PReal.lt_self_iff_mul_fact_lt_one (x y : ℝ>0) : x * y < x ↔ y < 1

theorem PReal.gt_add_right (x y : ℝ>0) : x + y > x

theorem PReal.div_lt_add_denum (x y z : ℝ>0) : x / (y + z) < x / y

theorem PReal.lt_iff_exists_add {x y : ℝ>0} (h : x < y) : ∃ (z : ℝ>0), y = x + z

theorem PReal.lt_iff_exists_add' {x y : ℝ>0} : x < y ↔ ∃ (z : ℝ>0), y = x + z

theorem PReal.sub_sub' (x y z : ℝ>0) (h : y + z < x) : x.sub (y + z) h = (x.sub y ⋯).sub z ⋯

theorem PReal.lt_imp_sub_lt (x y z : ℝ>0) (h : z < x) (h' : x < y) : x.sub z h < y

theorem PReal.x_sub_y_lt_x_sub_z_iff (x y z : ℝ>0) (h : z < x) (h' : y < x) : x.sub y h' < x.sub z h ↔ z < y

@[simp]

theorem PReal.add_sub (x y : ℝ>0) : (x + y).sub y ⋯ = x

theorem PReal.sub_lt_iff (x y z : ℝ>0) (h : y < x) : x.sub y h < z ↔ x < z + y

theorem PReal.add_lt_iff (x y z : ℝ>0) (h : x < z) : x + y < z ↔ y < z.sub x h

theorem PReal.sub_sub'' (x y z : ℝ>0) (h1 : z < y) (h2 : y.sub z h1 < x) : x.sub (y.sub z h1) h2 = (x + z).sub y ⋯

@[simp]

theorem PReal.sub_of_add (x y : ℝ>0) : (x + y).sub y ⋯ = x

theorem PReal.div_lt_div_same_num (a b c : ℝ>0) (hbc : b > c) : a / b < a / c

theorem PReal.div_lt_div_same_denum (a b c : ℝ>0) (hab : a < b) : a / c < b / c

theorem PReal.div_lt_div (a b c d : ℝ>0) (h_lt : a * d < b * c) : a / c < b / d

theorem PReal.div_lt_div_denum_right {d e : ℝ>0} (a b c : ℝ>0) : a / (b * c) < d / (e * c) ↔ a / b < d / e

theorem PReal.add_pos_of_Real (a b : ℝ>0) : ↑a + ↑b > 0

theorem PReal.mul_pos_of_Real (a b : ℝ>0) : ↑a * ↑b > 0

theorem PReal.neg_sub_ne_zero_pos {a b : ℝ} (h : a < b) : (a - b) ^ 2 > 0