no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.127506
G : Type ?u.127509
ι : Type ?u.127512
π : ι → Type ?u.127517
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
a x b c : E
⊢ a + x ∈ [a + b-[𝕜]a + c] ↔ x ∈ [b-[𝕜]c]
simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]