no goals
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 : P
⊢ ∠ p1 p2 p2 = π / 2
rw [angle_comm, angle_eq_left]