G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p1) +ᵥ p1 = 0 +ᵥ p1
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ -(p1 -ᵥ p2) = p2 -ᵥ p1
refine' neg_eq_of_add_eq_zero_right (vadd_right_cancel p1 _)
no goals
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p1) +ᵥ p1 = 0 +ᵥ p1
rw [vsub_add_vsub_cancel, vsub_self]