no goals
R : Type u_1
V : Type u_2
V' : Type ?u.554527
P : Type u_3
P' : Type ?u.554533
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₂ : 0 ≤ r₂
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
convert wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (r₁ • v +ᵥ x) v (Left.nonneg_neg_iff.2 hr₁)
    (neg_le_sub_iff_le_add.2 ((le_add_iff_nonneg_left r₁).2 hr₂)) using 1 <;>
  simp [sub_smul, ← add_vadd]