V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ arccos (inner x (-y) / (‖x‖ * ‖-y‖)) = π - arccos (inner x y / (‖x‖ * ‖y‖))
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ angle x (-y) = π - angle x y
unfold angle
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ arccos (inner x (-y) / (‖x‖ * ‖-y‖)) = π - arccos (inner x y / (‖x‖ * ‖y‖))
rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]