no goals
R : Type u_3
V : Type u_2
V' : Type ?u.49755
P : Type u_1
P' : Type ?u.49761
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : V
p : P
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]