no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.133397
G : Type ?u.133400
ι : Type ?u.133403
π : ι → Type ?u.133408
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]