no goals
R : Type u_2
V : Type u_1
V' : Type ?u.112580
P : Type ?u.112583
P' : Type ?u.112586
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 y : V
⊢ midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x
rw [midpoint_comm]
no goals
R : Type u_2
V : Type u_1
V' : Type ?u.112580
P : Type ?u.112583
P' : Type ?u.112586
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 y : V
⊢ midpoint R x y +ᵥ midpoint R y x = x + y
rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]