G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) +ᵥ p3 = p1 -ᵥ p3 +ᵥ p3
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3
apply vadd_right_cancel p3
no goals
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) +ᵥ p3 = p1 -ᵥ p3 +ᵥ p3
rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]