V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2
rw [← neg_eq_zero, ← inner_neg_right] at h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 2
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2
rw [sub_eq_add_neg]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 2
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0