no goals
α : Type u
β : Type v
X : Type ?u.237706
ι : Type ?u.237709
inst✝ : PseudoMetricSpace α
a b x✝ : ℝ≥0
⊢ nndist a b ≤ x✝ ↔ max (a - b) (b - a) ≤ x✝
simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, max_le_iff, abs_sub_le_iff,
  tsub_le_iff_right, NNReal.coe_add]