no goals
R : Type u_1
V : Type u_2
V' : Type ?u.542740
P : Type u_3
P' : Type ?u.542746
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
convert wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
    (neg_le_neg_iff.2 hr₂) using 1 <;>
  rw [neg_smul_neg]