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 p3 p4 p5 : P
hapc : ∠ p1 p5 p3 = π
hbpd : ∠ p2 p5 p4 = π
⊢ ∠ p1 p5 p2 = ∠ p3 p5 p4
linarith [angle_add_angle_eq_pi_of_angle_eq_pi p1 hbpd, angle_comm p4 p5 p1,
  angle_add_angle_eq_pi_of_angle_eq_pi p4 hapc, angle_comm p4 p5 p3]