R : Type u_1
V : Type u_2
V' : Type ?u.162563
P : Type u_3
P' : Type ?u.162569
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 : P
h : Wbtw R x y x
hne : y ≠ x
⊢ False
R : Type u_1
V : Type u_2
V' : Type ?u.162563
P : Type u_3
P' : Type ?u.162569
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 : P
h : Wbtw R x y z
hne : y ≠ z
⊢ x ≠ z
rintro rfl
R : Type u_1
V : Type u_2
V' : Type ?u.162563
P : Type u_3
P' : Type ?u.162569
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 : P
h : y = x
hne : y ≠ x
⊢ False
R : Type u_1
V : Type u_2
V' : Type ?u.162563
P : Type u_3
P' : Type ?u.162569
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 : P
h : Wbtw R x y x
hne : y ≠ x
⊢ False
rw [wbtw_self_iff] at h
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.162563
P : Type u_3
P' : Type ?u.162569
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 : P
h : y = x
hne : y ≠ x
⊢ False
exact hne h