V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = 0
⊢ ‖p1 -ᵥ ?p3 - (p3 -ᵥ ?p3)‖ = abs (‖p1 -ᵥ p2‖ - ‖p3 -ᵥ p2‖)

case p3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = 0
⊢ P
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = 0
⊢ dist p1 p3 = abs (dist p1 p2 - dist p3 p2)
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
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 : P
h : ∠ p1 p2 p3 = 0
⊢ ‖p1 -ᵥ ?p3 - (p3 -ᵥ ?p3)‖ = abs (‖p1 -ᵥ p2‖ - ‖p3 -ᵥ p2‖)

case p3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
h : ∠ p1 p2 p3 = 0
⊢ P
exact norm_sub_eq_abs_sub_norm_of_angle_eq_zero h