R : Type u_2
V : Type u_3
V' : Type ?u.622495
P : Type u_1
P' : Type ?u.622501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ x ≠ ↑(pointReflection R x) y
R : Type u_2
V : Type u_3
V' : Type ?u.622495
P : Type u_1
P' : Type ?u.622501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R y x (↑(pointReflection R x) y)
refine' ⟨wbtw_pointReflection _ _ _, h, _⟩
R : Type u_2
V : Type u_3
V' : Type ?u.622495
P : Type u_1
P' : Type ?u.622501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ ↑(pointReflection R x) x ≠ ↑(pointReflection R x) y
R : Type u_2
V : Type u_3
V' : Type ?u.622495
P : Type u_1
P' : Type ?u.622501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ x ≠ ↑(pointReflection R x) y
nth_rw 1 [← pointReflection_self R x]
no goals
R : Type u_2
V : Type u_3
V' : Type ?u.622495
P : Type u_1
P' : Type ?u.622501
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ ↑(pointReflection R x) x ≠ ↑(pointReflection R x) y
exact (pointReflection_involutive R x).injective.ne h