no goals
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2
rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]