R : Type u_1
V : Type u_2
V' : Type ?u.563494
P : Type u_3
P' : Type ?u.563500
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
R : Type u_1
V : Type u_2
V' : Type ?u.563494
P : Type u_3
P' : Type ?u.563500
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
rw [wbtw_comm]
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.563494
P : Type u_3
P' : Type ?u.563500
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
exact wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁