no goals
R : Type u_2
V : Type u_3
V' : Type ?u.99989
P : Type u_1
P' : Type ?u.99995
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 x x' y y' : P
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y
rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
  vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]