no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
r : ℝ
hr : r < 0
⊢ angle (r • x) y = angle (-x) y
rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]