α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b
α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
⊢ a ≤ b + nndist a b
suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
  rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b
α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b
rw [← sub_le_iff_le_add']
no goals
α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b
exact le_of_abs_le (dist_eq a b).ge
no goals
α : Type u
β : Type v
X : Type ?u.239808
ι : Type ?u.239811
inst✝ : PseudoMetricSpace α
a b : ℝ≥0
this : ↑a ≤ ↑b + dist a b
⊢ a ≤ b + nndist a b
rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]