no goals
R : Type u_1
V : Type u_2
V' : Type ?u.135022
P : Type u_3
P' : Type ?u.135028
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ direction s
⊢ SSameSide s (v +ᵥ x) y ↔ SSameSide s x y
rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]