G : Type u_2
P : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p3 -ᵥ p1 - (p3 -ᵥ p2)) = 0
G : Type u_2
P : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1
rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]
no goals
G : Type u_2
P : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p3 -ᵥ p1 - (p3 -ᵥ p2)) = 0
simp