no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.178821
G : Type ?u.178824
ι : Type ?u.178827
π : ι → Type ?u.178832
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ y ∈ openSegment 𝕜 x y ↔ x = y
rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]