def PReal.sub (x y : ℝ>0) (h : y < x) : ℝ>0

Equations

• x.sub y h = ⟨↑x - ↑y, ⋯⟩

@[simp]

theorem PReal.sub_toReal (x y : ℝ>0) (gt : y < x) : ↑(x.sub y gt) = ↑x - ↑y

@[simp]

theorem PReal.sub_toNNReal (x y : ℝ>0) (gt : y < x) : ↑(x.sub y gt) = ↑x - ↑y

@[simp]

theorem PReal.sub_y_add_y (x y : ℝ>0) (h : y < x) : x.sub y h + y = x

@[simp]

theorem PReal.add_y_sub_y (x y : ℝ>0) (h : y < x) : y + x.sub y h = x

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

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

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

theorem PReal.sub_div_aux (x y z : ℝ>0) (h : y < x * z) : y / z < x

theorem PReal.sub_div (x y z : ℝ>0) (h : y < x * z) : x.sub (y / z) ⋯ = (x * z).sub y h / z