no goals
R : Type u_2
V : Type u_1
V' : Type ?u.131151
P : Type ?u.131154
P' : Type ?u.131157
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x✝ y z : P
x : V
⊢ midpoint R x (-x) = 0
rw [midpoint_eq_smul_add, add_neg_self, smul_zero]