no goals
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
g : G
⊢ p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g
rw [← add_right_inj (p2 -ᵥ p1 : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ←
  add_sub_assoc, ← neg_vsub_eq_vsub_rev, neg_add_self, zero_sub]