V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
rw [← neg_eq_zero, ← inner_neg_right] at h
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]