x y : ℝ
h : x ≤ y
⊢ toNNReal x ≤ toNNReal y
x y : ℝ
h : x ≤ y
⊢ sqrt x ≤ sqrt y
rw [sqrt, sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt_iff]
no goals
x y : ℝ
h : x ≤ y
⊢ toNNReal x ≤ toNNReal y
exact toNNReal_le_toNNReal h