V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x + y) ≤ π / 2
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_two]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
exact div_nonneg (norm_nonneg _) (norm_nonneg _)