α : Type u_1
β : Type ?u.27664
inst✝ : EDist α
x y : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {y, x} ≤ edist y x
α : Type u_1
β : Type ?u.27664
inst✝ : EDist α
x y : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} ≤ edist y x
rw [pair_comm]
no goals
α : Type u_1
β : Type ?u.27664
inst✝ : EDist α
x y : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {y, x} ≤ edist y x
exact einfsep_pair_le_left hxy.symm